Commit daaf8139 authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

Logic is K or J rather than Classic,Intuiti

 Longer names are still accepted (as defined alias)
parent 7a02a82b
......@@ -1160,7 +1160,7 @@ Qed.
(** A few classical proofs *)
Lemma DoubleNeg A :
Pr Classic ([] ~~A -> A)%form.
Pr K ([] ~~A -> A).
Proof.
apply R_Imp_i.
apply R_Absu; trivial.
......@@ -1180,7 +1180,7 @@ Proof.
Qed.
Lemma Excluded_Middle A :
Pr Classic ([] A\/~A).
Pr K ([] A\/~A).
Proof.
apply R_Imp_e with (~~(A\/~A))%form.
- apply DoubleNeg.
......@@ -1188,7 +1188,7 @@ Proof.
Qed.
Lemma Peirce A B :
Pr Classic ([] ((A->B)->A)->A).
Pr K ([] ((A->B)->A)->A).
Proof.
apply R_Imp_i.
apply R_Absu; trivial.
......@@ -1266,7 +1266,7 @@ Definition Excluded_Middle_deriv A :=
(let '(Rule _ _ ds) := Excluded_Middle_core_deriv A in ds).
Lemma Excluded_Middle_valid A :
Valid Classic (Excluded_Middle_deriv A).
Valid K (Excluded_Middle_deriv A).
Proof.
unfold Excluded_Middle_deriv.
unfold Excluded_Middle_core_deriv.
......@@ -1275,7 +1275,7 @@ Qed.
(* A few examples of proofs in NJ1 and NK1 (Samuel). *)
Lemma ex1 f1 f2 : Provable Intuiti ([] (f1 /\ f2) -> (f1 \/ f2)).
Lemma ex1 f1 f2 : Provable J ([] (f1 /\ f2) -> (f1 \/ f2)).
Proof.
apply Provable_alt.
apply R_Imp_i.
......@@ -1285,7 +1285,7 @@ Proof.
apply in_eq.
Qed.
Lemma ex2 f1 f2 f3 : Provable Intuiti ([] (f1 -> f2 -> f3) <-> (f1 /\ f2 -> f3)).
Lemma ex2 f1 f2 f3 : Provable J ([] (f1 -> f2 -> f3) <-> (f1 /\ f2 -> f3)).
Proof.
apply Provable_alt.
apply R_And_i.
......@@ -1306,7 +1306,7 @@ Proof.
* apply in_eq.
Qed.
Lemma RAA f1 Γ : Pr Classic (Γ ~~f1) -> Pr Classic (Γ f1).
Lemma RAA f1 Γ : Pr K (Γ ~~f1) -> Pr K (Γ f1).
Proof.
intro.
apply R_Absu.
......@@ -1316,7 +1316,7 @@ Proof.
- apply Pr_pop. exact H.
Qed.
Lemma DeMorgan f1 f2 Γ : Pr Classic (Γ ~(~f1 /\ f2)) -> Pr Classic (Γ ~~(f1 \/ ~f2)).
Lemma DeMorgan f1 f2 Γ : Pr K (Γ ~(~f1 /\ f2)) -> Pr K (Γ ~~(f1 \/ ~f2)).
Proof.
intro.
apply R_Not_i.
......@@ -1338,7 +1338,7 @@ Proof.
+ apply Pr_pop. exact H.
Qed.
Lemma ExcludedMiddle f1 : Provable Classic ([] f1 \/ ~f1).
Lemma ExcludedMiddle f1 : Provable K ([] f1 \/ ~f1).
Proof.
apply Provable_alt.
apply RAA.
......
......@@ -586,7 +586,7 @@ Definition valid_deriv_step logic '(Rule r s ld) :=
&&& (A' =? bsubst 0 (FVar x) A)
&&& negb (Names.mem x (fvars (A::Γ⊢B)))
| Absu, s, [Not A::Γ ⊢ False] =>
(logic =? Classic) &&& (s =? (Γ ⊢ A))
(logic =? K) &&& (s =? (Γ ⊢ A))
| _,_,_ => false
end.
......@@ -601,12 +601,12 @@ Definition deriv_example :=
let A := Pred "A" [] in
Rule Imp_i ([]⊢A->A) [Rule Ax ([A]⊢A) []].
Compute valid_deriv Intuiti deriv_example.
Compute valid_deriv J deriv_example.
Definition example_gen (A:formula) :=
Rule Imp_i ([]⊢A->A) [Rule Ax ([A]⊢A) []].
Compute valid_deriv Intuiti (example_gen (Pred "A" [])).
Compute valid_deriv J (example_gen (Pred "A" [])).
Definition example2 (A B : term->formula):=
(Rule Imp_i ([]⊢(∀A(#0)/\B(#0))->(∀A(#0))/\(∀B(#0)))
......@@ -639,8 +639,8 @@ Definition em (A:formula) :=
;
Rule Ax ([~(A\/~A)]⊢~(A\/~A)) []]]%form.
Compute valid_deriv Classic (em (Pred "A" [])).
Compute valid_deriv Intuiti (em (Pred "A" [])).
Compute valid_deriv K (em (Pred "A" [])).
Compute valid_deriv J (em (Pred "A" [])).
(** Example of free alpha-renaming during a proof,
(not provable without alpha-renaming) *)
......@@ -651,7 +651,7 @@ Definition captcha :=
[Rule Imp_i ([A(FVar "x")]⊢A(FVar "z")->A(FVar "z"))
[Rule Ax ([A(FVar "z");A(FVar "x")]⊢A(FVar "z")) []]].
Compute valid_deriv Intuiti captcha.
Compute valid_deriv J captcha.
Definition captcha_bug :=
let A := fun x => Pred "A" [x] in
......@@ -659,7 +659,7 @@ Definition captcha_bug :=
[Rule Imp_i ([A(FVar "x")]⊢A(FVar "x")->A(FVar "x"))
[Rule Ax ([A(FVar "x");A(FVar "x")]⊢A(FVar "x")) []]].
Compute valid_deriv Intuiti captcha_bug.
Compute valid_deriv J captcha_bug.
(** Correctness of earlier boolean equality tests *)
......@@ -799,7 +799,7 @@ Inductive Valid (l:logic) : derivation -> Prop :=
Claim d1 (Γ ⊢ ∃A) -> Claim d2 ((bsubst 0 (FVar x) A)::Γ ⊢ B) ->
Valid l (Rule (Ex_e x) (Γ ⊢ B) [d1;d2])
| V_Absu d Γ A :
l=Classic ->
l=K ->
Valid l d -> Claim d (Not A :: Γ ⊢ False) ->
Valid l (Rule Absu (Γ ⊢ A) [d]).
......@@ -862,7 +862,7 @@ Definition Provable logic (s : sequent) :=
Lemma thm_example :
let A := Pred "A" [] in
Provable Intuiti ([]⊢A->A).
Provable J ([]⊢A->A).
Proof.
exists deriv_example. now rewrite <- Valid_equiv.
Qed.
......@@ -907,7 +907,7 @@ Inductive Pr (l:logic) : sequent -> Prop :=
| R_Ex_e x Γ A B : ~Names.In x (fvars (A::Γ⊢B)) ->
Pr l (Γ ⊢ ∃A) -> Pr l ((bsubst 0 (FVar x) A)::Γ ⊢ B) ->
Pr l (Γ ⊢ B)
| R_Absu Γ A : l=Classic -> Pr l (Not A :: Γ ⊢ False) ->
| R_Absu Γ A : l=K -> Pr l (Not A :: Γ ⊢ False) ->
Pr l (Γ ⊢ A).
Hint Constructors Pr.
......@@ -930,27 +930,27 @@ Qed.
(* Some useful statements. *)
Lemma Pr_intuit_classic s : Pr Intuiti s -> Pr Classic s.
Lemma Pr_intuit_classic s : Pr J s -> Pr K s.
Proof.
induction 1; eauto 2.
Qed.
Lemma Pr_intuit_any lg s : Pr Intuiti s -> Pr lg s.
Lemma Pr_intuit_any lg s : Pr J s -> Pr lg s.
Proof.
destruct lg. apply Pr_intuit_classic. trivial.
Qed.
Lemma Pr_any_classic lg s : Pr lg s -> Pr Classic s.
Lemma Pr_any_classic lg s : Pr lg s -> Pr K s.
Proof.
destruct lg. trivial. apply Pr_intuit_classic.
Qed.
Lemma intuit_classic d : Valid Intuiti d -> Valid Classic d.
Lemma intuit_classic d : Valid J d -> Valid K d.
Proof.
induction 1; eauto.
Qed.
Lemma any_classic d lg : Valid lg d -> Valid Classic d.
Lemma any_classic d lg : Valid lg d -> Valid K d.
Proof.
destruct lg. trivial. apply intuit_classic.
Qed.
......
......@@ -442,7 +442,7 @@ Definition valid_deriv_step logic '(Rule r s ld) :=
(s =? (Γ ⊢ B)) &&& (s1 =? (Γ ⊢ ∃x, A)) &&&
negb (Names.mem x (Seq.freevars s))
| Absu, s, [Not A::Γ ⊢ False] =>
(logic =? Classic) &&& (s =? (Γ ⊢ A))
(logic =? K) &&& (s =? (Γ ⊢ A))
| _,_,_ => false
end.
......@@ -455,7 +455,7 @@ Definition example :=
let A := Pred "A" [] in
Rule Imp_i ([]⊢A->A) [Rule Ax ([A]⊢A) []].
Compute valid_deriv Intuiti example.
Compute valid_deriv J example.
Definition example2 :=
let A := fun x => Pred "A" [Var x] in
......@@ -473,7 +473,7 @@ Definition example2 :=
[Rule (All_e (Var "x")) ([C]⊢A("x")/\B("x"))
[Rule Ax ([C]⊢C) []]]]]]).
Compute valid_deriv Intuiti example2.
Compute valid_deriv J example2.
Definition em :=
let A := Pred "A" [] in
......@@ -489,8 +489,8 @@ Definition em :=
;
Rule Ax ([~(A\/~A)]⊢~(A\/~A)) []]]%form.
Compute valid_deriv Classic em.
Compute valid_deriv Intuiti em.
Compute valid_deriv K em.
Compute valid_deriv J em.
(** Example of free alpha-renaming during a proof,
(not provable without alpha-renaming) *)
......@@ -501,7 +501,7 @@ Definition captcha :=
[Rule Imp_i ([A("x")]⊢A("z")->A("z"))
[Rule Ax ([A("z");A("x")]⊢A("z")) []]].
Compute valid_deriv Intuiti captcha.
Compute valid_deriv J captcha.
Definition captcha_bug :=
let A := fun x => Pred "A" [Var x] in
......@@ -509,7 +509,7 @@ Definition captcha_bug :=
[Rule Imp_i ([A("x")]⊢A("x")->A("x"))
[Rule Ax ([A("x");A("x")]⊢A("x")) []]].
Compute valid_deriv Intuiti captcha_bug.
Compute valid_deriv J captcha_bug.
(** Two early proofs : correctness of boolean equality on terms ... *)
......
......@@ -287,7 +287,7 @@ Ltac rec :=
(** Some basic proofs in Peano arithmetics. *)
Lemma ZeroRight :
IsTheorem Intuiti PeanoTheory
IsTheorem J PeanoTheory
( (#0 = #0 + Zero)).
Proof.
thm.
......@@ -305,7 +305,7 @@ Proof.
apply in_eq.
Qed.
Lemma SuccRight : IsTheorem Intuiti PeanoTheory (∀∀ (Succ(#1 + #0) = #1 + Succ(#0))).
Lemma SuccRight : IsTheorem J PeanoTheory (∀∀ (Succ(#1 + #0) = #1 + Succ(#0))).
Proof.
thm.
rec.
......@@ -331,7 +331,7 @@ Proof.
Qed.
Lemma Comm :
IsTheorem Intuiti PeanoTheory
IsTheorem J PeanoTheory
(( #0 = #0 + Zero) -> (∀∀ Succ(#1 + #0) = #1 + Succ(#0)) ->
(∀∀ #0 + #1 = #1 + #0)).
Proof.
......@@ -340,7 +340,7 @@ Proof.
+ app_R_All_i "x" x.
trans x.
- sym.
assert (Pr Intuiti (Γ' # 0 = # 0 + Zero)). { apply R_Ax. calc. }
assert (Pr J (Γ' # 0 = # 0 + Zero)). { apply R_Ax. calc. }
apply R_All_e with (t := x) in H; auto.
- sym.
inst_axiom ax9 [x].
......@@ -349,18 +349,18 @@ Proof.
app_R_All_i "x" x.
trans (Succ (x + y)).
- sym.
assert (Pr Intuiti (( #0 + y = y + #0) :: Γ' Succ (#1 + #0) = #1 + Succ (#0))). { apply R_Ax. calc. }
assert (Pr J (( #0 + y = y + #0) :: Γ' Succ (#1 + #0) = #1 + Succ (#0))). { apply R_Ax. calc. }
apply R_All_e with (t := x) in H; auto.
apply R_All_e with (t := y) in H; auto.
- trans (Succ (y + x)).
* ahered.
assert (Pr Intuiti (( #0 + y = y + #0) :: Γ' #0 + y = y + #0)). { apply R_Ax. apply in_eq. }
assert (Pr J (( #0 + y = y + #0) :: Γ' #0 + y = y + #0)). { apply R_Ax. apply in_eq. }
apply R_All_e with (t := x) in H; auto.
* sym.
inst_axiom ax10 [y; x].
Qed.
Lemma Commutativity : IsTheorem Intuiti PeanoTheory (∀∀ #0 + #1 = #1 + #0).
Lemma Commutativity : IsTheorem J PeanoTheory (∀∀ #0 + #1 = #1 + #0).
Proof.
apply ModusPonens with (A := (∀∀ Succ(#1 + #0) = #1 + Succ(#0))).
+ apply ModusPonens with (A := #0 = #0 + Zero).
......
......@@ -12,8 +12,6 @@ Import ListNotations.
Local Open Scope bool_scope.
Local Open Scope eqb_scope.
Notation K := Classic.
Implicit Types th : theory.
(** [downvars n = [#n ; ... ; #1] ]. *)
......
......@@ -617,7 +617,7 @@ Qed.
Lemma exex_tauto A :
level A <= 1 ->
Pr Classic ([] (( A) -> A)).
Pr K ([] (( A) -> A)).
Proof.
intros HA.
destruct (exist_fresh (fvars A)) as (x,Hx).
......@@ -637,7 +637,7 @@ Proof.
Qed.
Lemma exex_thm th A :
logic = Classic ->
logic = K ->
WC th (A) -> IsTheorem th ( (( A) -> A)).
Proof.
intros LG CL.
......@@ -865,7 +865,7 @@ Proof.
Qed.
Lemma HenkinSeq_consistent th nc n :
logic = Classic ->
logic = K ->
Consistent th <-> Consistent (HenkinSeq th nc n).
Proof.
intros LG.
......@@ -979,7 +979,7 @@ Qed.
(** TODO: conservative extention over th. Not that useful... *)
Lemma HenkinAll_consistent th (nc : NewCsts th) :
logic = Classic ->
logic = K ->
Consistent th -> Consistent (HenkinAll_ext th nc).
Proof.
intros LG C (_ & axs & F & V).
......@@ -992,7 +992,7 @@ Proof.
Qed.
Lemma HenkinAll_ext_supersaturated th (nc : NewCsts th) :
logic = Classic ->
logic = K ->
WitnessSuperSaturated (HenkinAll_ext th nc).
Proof.
red. intros LG A CL.
......@@ -1235,7 +1235,7 @@ Proof.
Qed.
Lemma supercomplete_consistent th nc :
logic = Classic ->
logic = K ->
Consistent th -> Consistent (supercomplete th nc).
Proof.
intros LG C.
......@@ -1244,7 +1244,7 @@ Proof.
Qed.
Lemma supercomplete_supersaturated th nc :
logic = Classic ->
logic = K ->
WitnessSuperSaturated (supercomplete th nc).
Proof.
intros LG.
......@@ -1256,7 +1256,7 @@ Proof.
Qed.
Lemma supercomplete_saturated th nc :
logic = Classic ->
logic = K ->
WitnessSaturated (supercomplete th nc).
Proof.
intros LG.
......@@ -1271,7 +1271,7 @@ Proof.
Qed.
Lemma supercompletion :
logic = Classic ->
logic = K ->
MyExcludedMiddle ->
forall th (nc : NewCsts th),
Consistent th ->
......
......@@ -31,14 +31,14 @@ Open Scope formula_scope.
(* It is easy to notice that a x (x a <-> ~(x x)) is (almost) an instance of the
comprehension axiom schema : it suffices to let A = ~ (a a). *)
Lemma Russell : Pr Intuiti ([ ∃∀ (#0 #1 <-> ~(#0 #0)) ] False).
Lemma Russell : Pr J ([ ∃∀ (#0 #1 <-> ~(#0 #0)) ] False).
Proof.
apply R'_Ex_e with (x := "a"); auto.
+ cbn - [Names.union]. intro. inversion H.
+ cbn. set (A := FVar "a"). fold (#0 A <-> ~ #0 #0)%form.
set (comp := _ <-> _).
set (Γ := [comp]).
assert (Pr Intuiti (Γ ~ A A)).
assert (Pr J (Γ ~ A A)).
{
apply R_Not_i.
set (Γ' := (_ :: Γ)).
......@@ -46,14 +46,14 @@ Proof.
* apply R_Ax. compute; intuition.
* apply R_Imp_e with (A := A A).
++ apply R_And_e1 with (B := (~ A A -> A A)).
assert (Pr Intuiti (Γ' comp)). { apply R_Ax. compute; intuition. }
assert (Pr J (Γ' comp)). { apply R_Ax. compute; intuition. }
apply R_All_e with (t := A) in H; auto.
++ apply R_Ax. compute; intuition.
}
apply R_Not_e with (A := A A); auto.
apply R_Imp_e with (A := ~ A A); auto.
- apply R_And_e2 with (A := (A A -> ~ A A)).
assert (Pr Intuiti (Γ comp)). { apply R_Ax. compute; intuition. }
assert (Pr J (Γ comp)). { apply R_Ax. compute; intuition. }
apply R_All_e with (t := A) in H0; auto.
Qed.
......@@ -175,7 +175,7 @@ Definition ZF :=
Import ZFAx.
Lemma emptyset : IsTheorem Intuiti ZF (∃∀ ~(#0 #1)).
Lemma emptyset : IsTheorem J ZF (∃∀ ~(#0 #1)).
Proof.
thm.
exists [infinity].
......@@ -196,7 +196,7 @@ Proof.
apply R'_Ax.
Qed.
Lemma singleton : IsTheorem Intuiti ZF (∀∃∀ (#0 #1 <-> #0 = #2)).
Lemma singleton : IsTheorem J ZF (∀∃∀ (#0 #1 <-> #0 = #2)).
Proof.
thm.
exists [pairing].
......@@ -223,7 +223,7 @@ Proof.
apply R_Or_i1; apply R_Ax; calc.
Qed.
Lemma unionset : IsTheorem Intuiti ZF (∀∀∃∀ (#0 #1 <-> #0 #3 \/ #0 #2)).
Lemma unionset : IsTheorem J ZF (∀∀∃∀ (#0 #1 <-> #0 #3 \/ #0 #2)).
Proof.
thm.
exists [ pairing; union; compat_right; eq_refl ].
......@@ -298,7 +298,7 @@ Proof.
-- apply R'_Ax.
Qed.
Lemma Succ : IsTheorem Intuiti ZF
Lemma Succ : IsTheorem J ZF
((∀∃∀ (#0 #1 <-> #0 = #2))
-> (∀∀∃∀ (#0 #1 <-> #0 #3 \/ #0 #2))
-> ∀∃ succ (#1) (#0)).
......@@ -345,7 +345,7 @@ Proof.
* apply R_Or_i2. apply R'_Ax.
Qed.
Lemma Successor : IsTheorem Intuiti ZF (∀∃ succ (#1) (#0)).
Lemma Successor : IsTheorem J ZF (∀∃ succ (#1) (#0)).
Proof.
apply ModusPonens with (A := ∀∀∃∀ #0 #1 <-> #0 #3 \/ #0 #2); [ | apply unionset ].
apply ModusPonens with (A := ∀∃∀ #0 #1 <-> #0 = #2); [ apply Succ | apply singleton ].
......
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