Finish pw07

1 files changed, 55 insertions, 29 deletions

diff --git a/pw07.v b/pw07.v
index d1711ae..35a03fd 100644
--- a/pw07.v
+++ b/pw07.v
@@ -55,23 +55,27 @@ Print example2.
 (* exercise 1: prove the lemma and inspect the proof term *)
 Lemma one : (forall x : Terms, P x) -> P M.
 Proof.
-(*! proof *)
-
+intro H.
+apply H.
 Qed.
+Print one.
 
 (* exercise 2: prove the lemma and inspect the proof term *)
 Lemma two : (A -> forall x : Terms, P x) -> forall y : Terms, A -> P y.
 Proof.
-(*! proof *)
-
+intros H y HA.
+apply H.
+assumption.
 Qed.
+Print two.
 
 (* exercise 3: prove the lemma and inspect the proof term *)
 Lemma three : A -> forall x : Terms, A.
 Proof.
-(*! proof *)
-
+intros H _.
+exact H.
 Qed.
+Print three.
 
 (* example, see slides 13-14-15 of week 7 *)
 Definition AS :=
@@ -100,22 +104,28 @@ Definition reflif := forall x : Terms, (exists y : Terms, R x y) -> R x x.
    define sym as the proposition stating that
    R is symmetric, that is,
    if x and y are related via R, then y and x are related via R *)
-Definition sym := (*! term *)
-  .
+Definition sym := forall x y : Terms, R x y -> R y x.
 
 (* exercise 5:
    define trans as the proposition stating that
    R is transitive, that is,
    if x and y are related via R, and y and z are related via R,
    then x and z are related via R  *)
-Definition trans := (*! term *)
-  .
+Definition trans := forall x y z : Terms, R x y /\ R y z -> R x z.
 
 (* exercise 6: prove the following Lemma *)
 Lemma str : sym -> trans -> reflif.
 Proof.
-(*! proof *)
-
+unfold sym.
+unfold trans.
+unfold reflif.
+intros Hsym Htrans x Hy.
+inversion Hy.
+apply Htrans with x0.
+split.
+assumption.
+apply Hsym.
+assumption.
 Qed.
 
 End pred1.
@@ -151,16 +161,23 @@ Parameter imp_elimination : forall p q : prop, T (p => q) -> T p -> T q.
 (* exercise 7 : prove the following lemma *)
 Lemma I : forall p : prop, T (p => p).
 Proof.
-(*! proof *)
-
+intro p.
+apply imp_introduction.
+intro.
+assumption.
 Qed.
 
 (* exercise 8 : prove the following lemma *)
 Lemma transitivity :
  forall p q r : prop, T (p => q) -> T (q => r) -> T (p => r).
 Proof.
-(*! proof *)
-
+intros p q r.
+intros H1 H2.
+apply imp_introduction.
+intro H3.
+apply imp_elimination with q.
+assumption.
+apply imp_elimination with p ; assumption.
 Qed.
 
 Parameter conjunction : prop -> prop -> prop.
@@ -169,20 +186,23 @@ Infix "X" := conjunction (no associativity, at level 90).
 (* exercise 9 : define variables that model the introduction
    rule for conjuction on prop, and both elimination rules *)
 
-Parameter conjunction_introduction : (*! term *)
-  .
+Parameter conjunction_introduction : forall p q : prop, T p -> T q -> T (p X q).
 
-Parameter conjunction_elimination_l : (*! term *)
-  .
+Parameter conjunction_elimination_l : forall p q : prop, T (p X q) -> T p.
 
-Parameter conjunction_elimination_r : (*! term *)
-  .
+Parameter conjunction_elimination_r : forall p q : prop, T (p X q) -> T q.
 
 (* exercise 10: prove the following lemma *)
 Lemma weak : forall a b c : prop, T (a => c) -> T ((a X b) => c).
 Proof.
-(*! proof *)
-
+intros a b c.
+intro.
+apply imp_introduction.
+intro.
+apply imp_elimination with a.
+assumption.
+apply conjunction_elimination_l with b.
+assumption.
 Qed.
 
 
@@ -198,10 +218,16 @@ Definition not (p : prop) := p => bot.
 (* exercise 11 : prove the following lemma *)
 Lemma contrapositive : forall p q : prop, T (p => q) -> T (not q => not p).
 Proof.
-(*! proof *)
-
+intros p q.
+intro.
+unfold not.
+apply imp_introduction.
+intro.
+apply imp_introduction.
+intro.
+apply imp_elimination with q.
+assumption.
+apply imp_elimination with p ; assumption.
 Qed.
 
-End logical_framework.
-
-
+End logical_framework.
\ No newline at end of file