Commit 87b2f2f8 authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

Mix : les temoins sont sans BVar

parent f3819e10
......@@ -332,7 +332,7 @@ Proof.
Qed.
Lemma mix_nam_mix_term t :
Mix.closed t ->
Mix.BClosed t ->
nam2mix_term [] (mix2nam_term [] t) = t.
Proof.
intros CL.
......@@ -341,10 +341,10 @@ Proof.
Qed.
Lemma mix_nam_mix f :
Mix.closed f ->
Mix.BClosed f ->
nam2mix [] (mix2nam [] f) = f.
Proof.
unfold Mix.closed. intros E.
unfold Mix.BClosed. intros E.
apply mix_nam_mix_gen; auto.
constructor.
simpl. rewrite E. auto.
......@@ -372,17 +372,17 @@ Proof.
- specialize (IHf (v::stack)). cbn in *. omega.
Qed.
Lemma nam2mix_term_closed t :
Mix.closed (nam2mix_term [] t).
Lemma nam2mix_term_bclosed t :
Mix.BClosed (nam2mix_term [] t).
Proof.
unfold Mix.closed.
unfold Mix.BClosed.
generalize (nam2mix_term_level [] t); simpl; omega.
Qed.
Lemma nam2mix_closed f :
Mix.closed (nam2mix [] f).
Lemma nam2mix_bclosed f :
Mix.BClosed (nam2mix [] f).
Proof.
unfold Mix.closed.
unfold Mix.BClosed.
generalize (nam2mix_level [] f). simpl. auto with *.
Qed.
......@@ -391,7 +391,7 @@ Lemma nam_mix_nam_term t :
Proof.
apply nam2mix_term_inj.
apply mix_nam_mix_term.
apply nam2mix_term_closed.
apply nam2mix_term_bclosed.
Qed.
Lemma nam_mix_nam f :
......@@ -399,7 +399,7 @@ Lemma nam_mix_nam f :
Proof.
apply nam2mix_canonical.
apply mix_nam_mix.
apply nam2mix_closed.
apply nam2mix_bclosed.
Qed.
Lemma AlphaEq_equivalence :
......
......@@ -159,8 +159,12 @@ Proof.
symmetry. apply nam2mix_altsubst_nop.
+ rewrite U, V, nam2mix_ctx_fvars.
rewrite nam2mix_fvars. simpl. varsdec.
- now rewrite nam2mix_subst_alt, nam2mix_altsubst_bsubst0.
- now rewrite nam2mix_subst_alt, nam2mix_altsubst_bsubst0.
- rewrite nam2mix_subst_alt, nam2mix_altsubst_bsubst0.
rewrite nam2mix_term_bclosed, eqb_refl.
apply andb_true_r.
- rewrite nam2mix_subst_alt, nam2mix_altsubst_bsubst0.
rewrite nam2mix_term_bclosed, eqb_refl.
apply andb_true_r.
- cbn.
apply eq_true_iff_eq.
rewrite !andb_true_iff.
......@@ -206,30 +210,30 @@ Proof.
Qed.
Lemma mix_nam_mix_rule (r:Mix.rule_kind) :
Mix.closed r ->
Mix.BClosed r ->
nam2mix_rule (mix2nam_rule r) = r.
Proof.
unfold Mix.closed.
unfold Mix.BClosed.
destruct r; cbn; intros CL; auto.
f_equal. apply mix_nam_mix_term, CL.
f_equal. apply mix_nam_mix_term, CL.
Qed.
Lemma mix_nam_mix_ctx (c:Mix.context) :
Mix.closed c ->
Mix.BClosed c ->
nam2mix_ctx (mix2nam_ctx c) = c.
Proof.
unfold Mix.closed.
unfold Mix.BClosed.
induction c as [|f c IH]; cbn; intros CL; auto.
apply max_0 in CL. destruct CL as (CL,CL').
f_equal; auto using mix_nam_mix.
Qed.
Lemma mix_nam_mix_seq (s:Mix.sequent) :
Mix.closed s ->
Mix.BClosed s ->
nam2mix_seq (mix2nam_seq s) = s.
Proof.
unfold Mix.closed.
unfold Mix.BClosed.
destruct s; cbn. intros CL.
apply max_0 in CL. destruct CL as (CL,CL').
f_equal.
......@@ -238,10 +242,10 @@ Proof.
Qed.
Lemma mix_nam_mix_deriv (d:Mix.derivation) :
Mix.closed d ->
Mix.BClosed d ->
nam2mix_deriv (mix2nam_deriv d) = d.
Proof.
unfold Mix.closed.
unfold Mix.BClosed.
induction d as [r s l IH] using Mix.derivation_ind'.
cbn; intros CL.
rewrite !max_0 in CL. destruct CL as (CL & CL' & CL'').
......@@ -255,7 +259,7 @@ Proof.
Qed.
Lemma mix2nam_valid_deriv logic (d:Mix.derivation) :
Mix.closed d ->
Mix.BClosed d ->
Nam.valid_deriv logic (mix2nam_deriv d) =
Mix.valid_deriv logic d.
Proof.
......@@ -263,31 +267,32 @@ Proof.
now rewrite <- nam2mix_valid_deriv, mix_nam_mix_deriv.
Qed.
(** nam2mix and closeness *)
(** nam2mix and BClosed *)
Lemma nam2mix_ctx_closed c : Mix.closed (nam2mix_ctx c).
Lemma nam2mix_ctx_bclosed c : Mix.BClosed (nam2mix_ctx c).
Proof.
unfold Mix.closed.
induction c; cbn; auto. rewrite nam2mix_closed. auto.
unfold Mix.BClosed.
induction c; cbn; auto. rewrite nam2mix_bclosed. auto.
Qed.
Lemma nam2mix_seq_closed s : Mix.closed (nam2mix_seq s).
Lemma nam2mix_seq_bclosed s : Mix.BClosed (nam2mix_seq s).
Proof.
unfold Mix.closed.
destruct s; cbn. now rewrite nam2mix_closed, nam2mix_ctx_closed.
unfold Mix.BClosed.
destruct s; cbn. now rewrite nam2mix_bclosed, nam2mix_ctx_bclosed.
Qed.
Lemma nam2mix_rule_closed r : Mix.closed (nam2mix_rule r).
Lemma nam2mix_rule_bclosed r : Mix.BClosed (nam2mix_rule r).
Proof.
unfold Mix.closed.
destruct r; cbn; auto; apply nam2mix_term_closed.
unfold Mix.BClosed.
destruct r; cbn; auto; apply nam2mix_term_bclosed.
Qed.
Lemma nam2mix_deriv_closed d : Mix.level (nam2mix_deriv d) = 0.
Lemma nam2mix_deriv_bclosed d : Mix.BClosed (nam2mix_deriv d).
Proof.
unfold Mix.BClosed.
revert d.
fix IH 1. destruct d as (r,s,l); cbn.
rewrite nam2mix_rule_closed, nam2mix_seq_closed. simpl.
rewrite nam2mix_rule_bclosed, nam2mix_seq_bclosed. simpl.
revert l.
fix IH' 1. destruct l as [|d l]; cbn; trivial.
rewrite IH. simpl. apply IH'.
......@@ -424,23 +429,23 @@ Qed.
Lemma nam_mix_nam_ctx c : AlphaEq_ctx (mix2nam_ctx (nam2mix_ctx c)) c.
Proof.
apply nam2mix_ctx_canonical, mix_nam_mix_ctx, nam2mix_ctx_closed.
apply nam2mix_ctx_canonical, mix_nam_mix_ctx, nam2mix_ctx_bclosed.
Qed.
Lemma nam_mix_nam_seq s : AlphaEq_seq (mix2nam_seq (nam2mix_seq s)) s.
Proof.
apply nam2mix_seq_canonical, mix_nam_mix_seq, nam2mix_seq_closed.
apply nam2mix_seq_canonical, mix_nam_mix_seq, nam2mix_seq_bclosed.
Qed.
Lemma nam_mix_nam_rule r : AlphaEq_rule (mix2nam_rule (nam2mix_rule r)) r.
Proof.
apply nam2mix_rule_canonical, mix_nam_mix_rule, nam2mix_rule_closed.
apply nam2mix_rule_canonical, mix_nam_mix_rule, nam2mix_rule_bclosed.
Qed.
Lemma nam_mix_nam_deriv d :
AlphaEq_deriv (mix2nam_deriv (nam2mix_deriv d)) d.
Proof.
apply nam2mix_deriv_canonical, mix_nam_mix_deriv, nam2mix_deriv_closed.
apply nam2mix_deriv_canonical, mix_nam_mix_deriv, nam2mix_deriv_bclosed.
Qed.
(** [Nam.valid_deriv] is compatible with alpha-equivalence *)
......
This diff is collapsed.
......@@ -106,9 +106,11 @@ Arguments vmap {_} {_} _ !_.
(** Some generic definitions based on the previous ones *)
Definition closed {A}`{Level A} (a:A) := level a = 0.
Definition BClosed {A}`{Level A} (a:A) := level a = 0.
Hint Unfold closed.
Definition FClosed {A}`{FVars A} (a:A) := Vars.Empty (fvars a).
Hint Unfold BClosed FClosed.
(** Substitution of a free variable in a term :
in [t], free var [v] is replaced by [u]. *)
......@@ -314,6 +316,14 @@ Instance form_level : Level formula :=
| Pred _ args => list_max (map level args)
end.
(** Important note : [bsubst] below is only intended to be
used with a replacement term [t] with no bounded variables !
In a full De Bruijn implementation, we would tweak [t]
(i.e. "lift" it) when entering a quantified part of a formula.
Here it's much simpler to *not* do it, but this may lead to
unexpected results if [t] still has some bounded variables,
see later the treatment of rules ∀e and ∃i. *)
Instance form_bsubst : BSubst formula :=
fix form_bsubst n t f :=
match f with
......@@ -426,7 +436,7 @@ Inductive derivation :=
Definition claim '(Rule _ s _) := s.
(** Utility functions on derivations:
- bounded-vars level (used by the [closed] predicate),
- bounded-vars level (used by the [BClosed] predicate),
- check w.r.t. signature *)
Instance level_rule_kind : Level rule_kind :=
......@@ -496,6 +506,24 @@ Instance vmap_rule : VMap rule_kind :=
(** Validity of a derivation : is it using correct rules
of classical logic (resp. intuitionistic logic) ? *)
(** Note that we require the witness terms in rules ∀e and ∃i
to be [BClosed] (i.e. without any [BVar]). Otherwise
awkward things may happen due to our implementation
of [bsubst].
For instance think of [∀ ∃ ~(Pred "=" [#0;#1])] i.e.
[∀x∃y,x≠y], a possible way of saying that the world isn't
a singleton. With an unrestricted ∀e, we could deduce
[bsubst 0 (#0) (∃ ~(Pred "=" [#0;#1]))] which reduces
to [∃ ~(Pred "=" [#0;#0])], a formula negating the reflexivity
of equality !
Apart from these witnesses, the rest of the derivation
could technically have unbounded variables, even though
we intend all derivations to be [BClosed]. We will be able
to force this later on (see [Meta.forcelevel])
*)
Definition valid_deriv_step logic '(Rule r s ld) :=
match r, s, List.map claim ld with
| Ax, (Γ ⊢ A), [] => list_mem A Γ
......@@ -519,9 +547,9 @@ Definition valid_deriv_step logic '(Rule r s ld) :=
(Γ =? Γ') &&& (A' =? bsubst 0 (FVar x) A)
&&& negb (Vars.mem x (fvars (Γ⊢A)))
| All_e t, (Γ ⊢ B), [Γ'⊢ ∀A] =>
(Γ =? Γ') &&& (B =? bsubst 0 t A)
(Γ =? Γ') &&& (B =? bsubst 0 t A) &&& (level t =? 0)
| Ex_i t, (Γ ⊢ ∃A), [Γ'⊢B] =>
(Γ =? Γ') &&& (B =? bsubst 0 t A)
(Γ =? Γ') &&& (B =? bsubst 0 t A) &&& (level t =? 0)
| Ex_e x, s, [Γ⊢∃A; A'::Γ'⊢B] =>
(s =? (Γ ⊢ B)) &&& (Γ' =? Γ)
&&& (A' =? bsubst 0 (FVar x) A)
......@@ -729,10 +757,10 @@ Inductive Valid (l:logic) : derivation -> Prop :=
Valid l d -> Claim d (Γ ⊢ bsubst 0 (FVar x) A) ->
Valid l (Rule (All_i x) (Γ ⊢ ∀A) [d])
| V_All_e t d Γ A :
Valid l d -> Claim d (Γ ⊢ ∀A) ->
BClosed t -> Valid l d -> Claim d (Γ ⊢ ∀A) ->
Valid l (Rule (All_e t) (Γ ⊢ bsubst 0 t A) [d])
| V_Ex_i t d Γ A :
Valid l d -> Claim d (Γ ⊢ bsubst 0 t A) ->
BClosed t -> Valid l d -> Claim d (Γ ⊢ bsubst 0 t A) ->
Valid l (Rule (Ex_i t) (Γ ⊢ ∃A) [d])
| V_Ex_e x d1 d2 Γ A B :
~Vars.In x (fvars (A::Γ⊢B)) ->
......@@ -770,7 +798,7 @@ Ltac mytac :=
rewrite ?@eqb_eq in * by auto with typeclass_instances.
Ltac rewr :=
unfold Claim in *;
unfold Claim, BClosed in *;
match goal with
| H: _ = _ |- _ => rewrite H in *; clear H; rewr
| _ => rewrite ?eqb_refl
......@@ -811,7 +839,8 @@ Qed.
(** A provability notion directly on sequents, without derivations.
Pros: lighter
Cons: no easy way to say later that the whole proof is closed *)
Cons: no easy way to express meta-theoretical facts about the proof
itself (e.g. free or bounded variables used during the proof). *)
Inductive Pr (l:logic) : sequent -> Prop :=
| R_Ax Γ A : In A Γ -> Pr l (Γ ⊢ A)
......@@ -842,10 +871,10 @@ Inductive Pr (l:logic) : sequent -> Prop :=
| R_All_i x Γ A : ~Vars.In x (fvars (Γ ⊢ A)) ->
Pr l (Γ ⊢ bsubst 0 (FVar x) A) ->
Pr l (Γ ⊢ ∀A)
| R_All_e t Γ A : Pr l (Γ ⊢ ∀A) ->
Pr l (Γ ⊢ bsubst 0 t A)
| R_Ex_i t Γ A : Pr l (Γ ⊢ bsubst 0 t A) ->
Pr l (Γ ⊢ ∃A)
| R_All_e t Γ A : BClosed t -> Pr l (Γ ⊢ ∀A) ->
Pr l (Γ ⊢ bsubst 0 t A)
| R_Ex_i t Γ A : BClosed t -> Pr l (Γ ⊢ bsubst 0 t A) ->
Pr l (Γ ⊢ ∃A)
| R_Ex_e x Γ A B : ~Vars.In x (fvars (A::Γ⊢B)) ->
Pr l (Γ ⊢ ∃A) -> Pr l ((bsubst 0 (FVar x) A)::Γ ⊢ B) ->
Pr l (Γ ⊢ B)
......
......@@ -14,4 +14,7 @@ General
- Peut-on éviter tous ces "fix IH 1" ??
- Integrer closed dans Valid et valid_deriv ??
X Integrer closed dans Valid et valid_deriv ??
ToCoq : revoir a se passer de BClosed general,
maintenant que Valid impose des temoins BClosed
\ No newline at end of file
......@@ -7,10 +7,10 @@ Local Open Scope bool_scope.
Local Open Scope eqb_scope.
Definition ClosedFormulaOn (sign:gen_signature) (A:formula) :=
check sign A = true /\ closed A /\ Vars.Empty (fvars A).
check sign A = true /\ BClosed A /\ FClosed A.
Definition ValidDerivOn logic (sign:gen_signature) d :=
check sign d = true /\ closed d /\ Valid logic d.
check sign d = true /\ BClosed d /\ Valid logic d.
Record theory :=
{ sign :> gen_signature;
......@@ -41,8 +41,46 @@ Definition IsTheorem th T :=
Lemma thm_alt th T :
IsTheorem th T <-> IsTheoremStrict th T.
Proof.
(* Cf preuve a finir dans Meta *)
Admitted.
split.
- intros (CL & axs & F & PR).
split; auto. rewrite Provable_alt in PR. destruct PR as (d & V & C).
assert (Hx := fresh_var_ok (fvars d)).
set (x := fresh_var (fvars d)) in *.
assert (Hy := fresh_var_ok (Vars.add x (fvars d))).
set (y := fresh_var (Vars.add x (fvars d))) in *.
exists (forcelevel_deriv y (restrict_deriv th x d)).
exists axs; repeat split; auto.
+ rewrite <- restrict_forcelevel_deriv.
apply restrict_deriv_check.
+ apply forcelevel_deriv_bclosed.
+ apply forcelevel_deriv_valid.
* rewrite restrict_deriv_fvars.
varsdec.
* apply restrict_valid; auto.
+ rewrite Forall_forall in F.
unfold Claim.
rewrite claim_forcelevel, claim_restrict, C.
cbn. f_equal.
* assert (check th axs = true).
{ unfold check, check_list.
apply forallb_forall.
intros A HA. apply WfAxiom; auto. }
rewrite check_restrict_ctx_id by auto.
apply forcelevel_ctx_id.
unfold BClosed, level, level_list.
apply list_max_map_0.
intros A HA. apply (WfAxiom th A); auto.
* rewrite check_restrict_id by apply CL.
apply forcelevel_id.
assert (level T = 0) by apply CL.
auto with *.
- intros (CL & d & axs & V & F & C).
split; auto.
exists axs; split; auto.
rewrite Provable_alt.
exists d; split; auto.
apply V.
Qed.
Lemma ax_thm th A : IsAxiom th A -> IsTheorem th A.
Proof.
......@@ -147,7 +185,7 @@ Definition IsEqualityTheory th :=
IsTheorem th (Pred "=" [#0; #0])%form /\
forall A z,
check (th.(sign)) A = true ->
closed A ->
BClosed A ->
Vars.Equal (fvars A) (Vars.singleton z) ->
IsTheorem th (∀∀(Pred "=" [#1;#0] -> fsubst z (#1) A -> fsubst z (#0) A))%form.
......@@ -173,8 +211,9 @@ Proof.
Qed.
(** If we only extend the signature, not the axioms, then
it's a conservative extension. To prove this, we restrict
derivations to the small signature. *)
it's a conservative extension.
To prove this, normally we restrict a proof to the small
signature, but here with [Pr] it's implicit (see thm_alt) *)
Lemma ext_sign_only th1 th2 :
SignExtend th1 th2 ->
......@@ -186,26 +225,8 @@ Proof.
intros A. rewrite EQ. apply ax_thm.
- intros T (CL & axs & F & PR) CK. split.
+ split; auto. apply CL.
+ exists axs. split.
* rewrite Forall_forall in *. intros x Hx. rewrite EQ; auto.
* auto.
(* normally we should adapt the proof to use only
th1.(sign), thanks to [restrict] and co.
But the Pr relation doesn't care... *)
(*
rewrite Provable_alt in *. unfold Provable in *.
destruct PR as (d & V & C).
assert (Hx := fresh_var_ok (fvars d)).
set (x := fresh_var (fvars d)) in *. clearbody x.
exists (restrict_deriv th1 x d); split.
{ apply restrict_valid; auto. }
{ unfold Claim. rewrite claim_restrict, C. cbn; f_equal.
- unfold restrict_ctx. apply map_id_iff.
intros A HA. apply restrict_check.
apply th1.(WfAxiom). rewrite EQ.
rewrite Forall_forall in F; auto.
- apply restrict_check; auto. }
*)
+ exists axs. split; auto.
rewrite Forall_forall in *. intros x Hx. rewrite EQ; auto.
Qed.
(** Henkin extension : adding a new constant as witness
......@@ -245,8 +266,9 @@ Proof.
{ apply level_bsubst; auto.
assert (level ( A)%form = 0) by apply CL.
cbn in *. omega. }
unfold closed; omega.
+ rewrite bsubst_fvars. cbn - [Vars.union].
unfold BClosed; omega.
+ unfold FClosed.
rewrite bsubst_fvars. cbn - [Vars.union].
intro v. VarsF.set_iff.
assert (Vars.Empty (fvars ( A)%form)) by apply CL.
varsdec.
......@@ -288,18 +310,13 @@ Proof.
rewrite negb_true_iff, eqb_neq.
intros [(IN,NE)|IN]; auto. apply F in IN. cbn in IN.
unfold Henkin_axiom in IN; intuition.
* (* TODO: restrict ? *)
assert (Pr logic (newAx::axs' T)).
* assert (Pr logic (newAx::axs' T)).
{ eapply Pr_weakening; eauto.
constructor. unfold axs'.
intros v. simpl. rewrite filter_In.
rewrite negb_true_iff, eqb_neq.
destruct (eqbspec v newAx); intuition. }
apply R_Ex_e with "x"%string A.
{ admit. }
{ apply Pr_weakening with (axsA ( A)); auto.
constructor. intros a. rewrite in_app_iff; auto. }
{ admit. }
(* Todo : restrict sur H pour en faire du A(x) ... |- T *)
Admitted.
(** Completeness of a theory *)
......
......@@ -158,17 +158,17 @@ Proof.
Qed.
Lemma interp_term_closed genv lenv t :
closed t ->
BClosed t ->
interp_term genv lenv t = interp_term genv [] t.
Proof.
unfold closed. intros E.
unfold BClosed. intros E.
apply (interp_term_more_lenv genv [] lenv). simpl. auto with *.
Qed.
Lemma interp_term_bsubst genv lenv u m n t :
level t <= S n ->
List.length lenv = n ->
closed u ->
BClosed u ->
interp_term genv [] u = m ->
interp_term genv (lenv++[m]) t =
interp_term genv lenv (bsubst n u t).
......@@ -189,7 +189,7 @@ Qed.
Lemma interp_form_bsubst genv lenv u m n f :
level f <= S n ->
List.length lenv = n ->
closed u ->
BClosed u ->
interp_term genv [] u = m ->
interp_form genv (lenv++[m]) f <-> interp_form genv lenv (bsubst n u f).
Proof.
......@@ -215,7 +215,7 @@ Qed.
Lemma interp_form_bsubst0 genv u m f :
level f <= 1 ->
closed u ->
BClosed u ->
interp_term genv [] u = m ->
interp_form genv [m] f <-> interp_form genv [] (bsubst 0 u f).
Proof.
......@@ -281,10 +281,10 @@ Ltac substClaim :=
Lemma correctness (logic:Defs.logic)(d:derivation) :
CoqRequirements logic ->
Valid logic d ->
closed d ->
BClosed d ->
forall genv, interp_seq genv [] (claim d).
Proof.
unfold closed.
unfold BClosed.
intros CR.
induction 1; intros CL genv Hc; substClaim;
cbn in CL; rewrite ?eqb_eq, ?max_0 in CL;
......@@ -315,7 +315,7 @@ Qed.
Lemma coherence logic : CoqRequirements logic ->
forall (d:derivation),
Valid logic d ->
closed d ->
BClosed d ->
~Claim d ([]False).
Proof.
intros CR d VD CL E.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment