Commit 4671d5bb authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

Deplacement d'essais de derivations par Samuel à la fin de Meta.v

parent 4b3a4060
......@@ -1832,3 +1832,79 @@ Proof.
- rewrite !map_map. apply map_ext_iff.
rewrite Forall_forall in IH; auto.
Qed.
(* A few examples of proofs in NJ1 and NK1 (Samuel). *)
Lemma ex1 f1 f2 : Provable Intuiti ([] (f1 /\ f2) -> (f1 \/ f2)).
Proof.
apply Provable_alt.
apply R_Imp_i.
apply R_Or_i1.
apply R_And_e1 with (B := f2).
apply R_Ax.
apply in_eq.
Qed.
Lemma ex2 f1 f2 f3 : Provable Intuiti ([] (f1 -> f2 -> f3) <-> (f1 /\ f2 -> f3)).
Proof.
apply Provable_alt.
apply R_And_i.
+ apply R_Imp_i.
apply R_Imp_i.
apply R_Imp_e with (A := f2).
- apply R_Imp_e with (A := f1).
* apply R_Ax. apply in_cons. apply in_eq.
* apply R_And_e1 with (B := f2). apply R_Ax. apply in_eq.
- apply R_And_e2 with (A := f1). apply R_Ax. apply in_eq.
+ apply R_Imp_i.
apply R_Imp_i.
apply R_Imp_i.
apply R_Imp_e with (A := (f1 /\ f2)%form).
- apply R_Ax. apply in_cons. apply in_cons. apply in_eq.
- apply R_And_i; apply R_Ax.
* apply in_cons. apply in_eq.
* apply in_eq.
Qed.
Lemma RAA f1 Γ : Pr Classic (Γ ~~f1) -> Pr Classic (Γ f1).
Proof.
intro.
apply R_Absu.
+ reflexivity.
+ apply R_Not_e with (A := (~ f1)%form).
- apply R_Ax. apply in_eq.
- apply Pr_pop. exact H.
Qed.
Lemma DeMorgan f1 f2 Γ : Pr Classic (Γ ~(~f1 /\ f2)) -> Pr Classic (Γ ~~(f1 \/ ~f2)).
Proof.
intro.
apply R_Not_i.
apply R_Not_e with (A := (~f1 /\ f2)%form).
+ apply RAA with (f1 := (~f1 /\ f2)%form).
apply R_Not_i.
apply R_Not_e with (A := (f1\/~f2)%form).
- apply R_Or_i1.
apply RAA.
apply R_Not_i.
apply R_Not_e with (A := (f1\/~f2)%form).
* apply R_Or_i2. apply R_Not_i. apply R_Not_e with (A := (~f1 /\ f2)%form).
++ apply R_And_i.
-- apply R_Ax. apply in_cons. apply in_eq.
-- apply R_Ax. apply in_eq.
++ apply R_Ax. apply in_cons. apply in_cons. apply in_eq.
* apply R_Ax. apply in_cons. apply in_cons. apply in_eq.
- apply R_Ax. apply in_cons. apply in_eq.
+ apply Pr_pop. exact H.
Qed.
Lemma ExcludedMiddle f1 : Provable Classic ([] f1 \/ ~f1).
Proof.
apply Provable_alt.
apply RAA.
apply DeMorgan with (f2 := f1) (Γ := []).
apply R_Not_i.
apply R_Not_e with (A := f1).
+ apply R_And_e2 with (A := (~f1)%form). apply R_Ax. apply in_eq.
+ apply R_And_e1 with (B := f1). apply R_Ax. apply in_eq.
Qed.
......@@ -909,86 +909,7 @@ Proof.
- intros (d & Hd & <-). now apply Valid_Pr.
Qed.
(* A few examples of proofs in NJ1 and NK1. *)
Lemma ex1 f1 f2 : Provable Intuiti ([] ⊢ (f1 /\ f2) -> (f1 \/ f2)).
Proof.
apply Provable_alt.
apply R_Imp_i.
apply R_Or_i1.
apply R_And_e1 with (B := f2).
apply R_Ax.
apply in_eq.
Qed.
Lemma ex2 f1 f2 f3 : Provable Intuiti ([] ⊢ (f1 -> f2 -> f3) <-> (f1 /\ f2 -> f3)).
Proof.
apply Provable_alt.
apply R_And_i.
+ apply R_Imp_i.
apply R_Imp_i.
apply R_Imp_e with (A := f2).
- apply R_Imp_e with (A := f1).
* apply R_Ax. apply in_cons. apply in_eq.
* apply R_And_e1 with (B := f2). apply R_Ax. apply in_eq.
- apply R_And_e2 with (A := f1). apply R_Ax. apply in_eq.
+ apply R_Imp_i.
apply R_Imp_i.
apply R_Imp_i.
apply R_Imp_e with (A := (f1 /\ f2)%form).
- apply R_Ax. apply in_cons. apply in_cons. apply in_eq.
- apply R_And_i; apply R_Ax.
* apply in_cons. apply in_eq.
* apply in_eq.
Qed.
Lemma Weakening Γ f2 lg : forall f1, Pr lg (Γ ⊢ f1) -> Pr lg (f2::Γ ⊢ f1).
Admitted.
Lemma RAA f1 Γ : Pr Classic (Γ ⊢ ~~f1) -> Pr Classic (Γ ⊢ f1).
Proof.
intro.
apply R_Absu.
+ reflexivity.
+ apply R_Not_e with (A := (~ f1)%form).
- apply R_Ax. apply in_eq.
- apply Weakening. exact H.
Qed.
Lemma DeMorgan f1 f2 Γ : Pr Classic (Γ ⊢ ~(~f1 /\ f2)) -> Pr Classic (Γ ⊢ ~~(f1 \/ ~f2)).
Proof.
intro.
apply R_Not_i.
apply R_Not_e with (A := (~f1 /\ f2)%form).
+ apply RAA with (f1 := (~f1 /\ f2)%form).
apply R_Not_i.
apply R_Not_e with (A := (f1\/~f2)%form).
- apply R_Or_i1.
apply RAA.
apply R_Not_i.
apply R_Not_e with (A := (f1\/~f2)%form).
* apply R_Or_i2. apply R_Not_i. apply R_Not_e with (A := (~f1 /\ f2)%form).
++ apply R_And_i.
-- apply R_Ax. apply in_cons. apply in_eq.
-- apply R_Ax. apply in_eq.
++ apply R_Ax. apply in_cons. apply in_cons. apply in_eq.
* apply R_Ax. apply in_cons. apply in_cons. apply in_eq.
- apply R_Ax. apply in_cons. apply in_eq.
+ apply Weakening. exact H.
Qed.
Lemma ExcludedMiddle f1 : Provable Classic ([] ⊢ f1 \/ ~f1).
Proof.
apply Provable_alt.
apply RAA.
apply DeMorgan with (f2 := f1) (Γ := []).
apply R_Not_i.
apply R_Not_e with (A := f1).
+ apply R_And_e2 with (A := (~f1)%form). apply R_Ax. apply in_eq.
+ apply R_And_e1 with (B := f1). apply R_Ax. apply in_eq.
Qed.
(* Some usefull statements. *)
(* Some useful statements. *)
Lemma Pr_intuit_classic s : Pr Intuiti s -> Pr Classic s.
Proof.
......
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