diff options
| -rw-r--r-- | pw07.v | 84 |
1 files changed, 55 insertions, 29 deletions
@@ -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 |