From 6482186773136bfef15a3f095933362e8b1135ee Mon Sep 17 00:00:00 2001 From: Yadunand Prem Date: Sun, 4 Feb 2024 15:40:50 +0800 Subject: [PATCH] feat: 3234 week 2 --- ...eek-01_functional-programming-in-Gallina.v | 47 +- cs3234/labs/week-01_polymorphism.v | 180 ++++++ cs3234/labs/week-02_exercises.v | 215 +++++++ .../week-02_formalizing-a-proof-in-tcpa.v | 325 +++++++++++ .../labs/week-02_proving-logical-properties.v | 539 ++++++++++++++++++ cs3234/labs/week-02_the-intro-tactic.v | 110 ++++ cs3234/labs/week-02_the-revert-tactic.v | 67 +++ 7 files changed, 1438 insertions(+), 45 deletions(-) create mode 100644 cs3234/labs/week-01_polymorphism.v create mode 100644 cs3234/labs/week-02_exercises.v create mode 100644 cs3234/labs/week-02_formalizing-a-proof-in-tcpa.v create mode 100644 cs3234/labs/week-02_proving-logical-properties.v create mode 100644 cs3234/labs/week-02_the-intro-tactic.v create mode 100644 cs3234/labs/week-02_the-revert-tactic.v diff --git a/cs3234/labs/week-01_functional-programming-in-Gallina.v b/cs3234/labs/week-01_functional-programming-in-Gallina.v index 2cd78fa..0fc55b1 100644 --- a/cs3234/labs/week-01_functional-programming-in-Gallina.v +++ b/cs3234/labs/week-01_functional-programming-in-Gallina.v @@ -5,50 +5,6 @@ (* was: *) (* Version of 18 Jan 2024 *) -(* ********** *) - -(* name: - e-mail address: - student number: - *) - -(* name: - e-mail address: - student number: - *) - -(* name: - e-mail address: - student number: - *) - -(* name: - e-mail address: - student number: - *) - -(* name: - e-mail address: - student number: - *) - -(* name: - e-mail address: - student number: - *) - -(* name: - e-mail address: - student number: - *) - -(* name: - e-mail address: - student number: - *) - -(* ********** *) - Check 0. Check O. @@ -309,7 +265,8 @@ Definition test_mult (candidate: nat -> nat -> nat) : bool := (let x := 5 in let y := 6 in let z := 7 in - (Nat.eqb (candidate x (candidate y z)) (candidate z (candidate x y)))) + (Nat.eqb (candidate x (candidate y z)) + (candidate (candidate x y) z))) && ( (* Testing the inductive step *) diff --git a/cs3234/labs/week-01_polymorphism.v b/cs3234/labs/week-01_polymorphism.v new file mode 100644 index 0000000..7608cb5 --- /dev/null +++ b/cs3234/labs/week-01_polymorphism.v @@ -0,0 +1,180 @@ +(* week-01_polymorphism.v *) +(* LPP 2024 - CS3234 2023-2024, Sem2 *) +(* Olivier Danvy *) +(* Version of 18 Jan 2024 *) + +(* ********** *) + +Require Import Arith Bool. + +(* ********** *) + +Definition make_pair_v0 : forall (A : Type) (B : Type), A -> B -> A * B := + fun A B a b => (a, b). + +Definition make_pair_v1 (A : Type) : forall B : Type, A -> B -> A * B := + fun B a b => (a, b). + +Definition make_pair_v2 (A : Type) (B : Type) : A -> B -> A * B := + fun a b => (a, b). + +Definition make_pair_v3 (A : Type) (B : Type) (a : A) : B -> A * B := + fun b => (a, b). + +Definition make_pair_v4 (A : Type) (B : Type) (a : A) (b : B) : A * B := + (a, b). + +(* ***** *) +Compute make_pair_v0 nat bool 1 true. + +Compute (make_pair_v4 nat bool 1 true). +(* = (1, true) : nat * bool *) + +Definition dupl (V : Type) (v : V) : V * V := + make_pair_v4 V V v v. + +(* ********** *) + +Inductive polymorphic_binary_tree (V : Type) : Type := +| PLeaf : V -> polymorphic_binary_tree V +| PNode : polymorphic_binary_tree V -> polymorphic_binary_tree V -> polymorphic_binary_tree V. + +Definition test_number_of_leaves (candidate : forall V : Type, polymorphic_binary_tree V -> nat) := + (candidate bool (PLeaf bool true) =? 1) && + (candidate nat (PNode nat (PLeaf nat 0) (PLeaf nat 1)) =? 2). + +Fixpoint number_of_leaves (V : Type) (t : polymorphic_binary_tree V) : nat := + match t with + | PLeaf _ v => + 1 + | PNode _ t1 t2 => + number_of_leaves V t1 + number_of_leaves V t2 + end. + +Compute (test_number_of_leaves number_of_leaves). + +(* ********** *) + +Fixpoint eqb_polymorphic_binary_tree (V : Type) (eqb_V : V -> V -> bool) (t1 t2 : polymorphic_binary_tree V) : bool := + match t1 with + | PLeaf _ v1 => + match t2 with + | PLeaf _ v2 => + eqb_V v1 v2 + | PNode _ t11 t12 => + false + end + | PNode _ t11 t12 => + match t2 with + | PLeaf _ v2 => + false + | PNode _ t21 t22 => + eqb_polymorphic_binary_tree V eqb_V t11 t21 + && + eqb_polymorphic_binary_tree V eqb_V t12 t22 + end + end. + +(* ********** *) + +Definition eqb_nat := Nat.eqb. + +Definition eqb_binary_tree_of_nats (t1 t2 : polymorphic_binary_tree nat) : bool := + eqb_polymorphic_binary_tree nat eqb_nat t1 t2. + +(* ********** *) + +(* Exercise 05 *) +Definition e5a : polymorphic_binary_tree (nat * bool) := + PNode (nat * bool) + (PLeaf (nat * bool) (0, true)) + (PLeaf (nat * bool) (1, false)) +. + +Check e5a. +Compute e5a. + +Definition nTree := (polymorphic_binary_tree nat). + +Definition e5b : polymorphic_binary_tree (polymorphic_binary_tree nat) := + PNode (nTree) + (PLeaf (nTree) (PLeaf nat 1)) + (PLeaf (nTree) (PLeaf nat 2)) +. + +Check e5b. +Compute e5b. +(* Exercise 07 *) + +Definition eqb_option (V : Type) (eqb_V : V -> V -> bool) (ov1 ov2 : option V) : bool := + match ov1 with + | Some v1 => + match ov2 with + | Some v2 => + eqb_V v1 v2 + | None => + false + end + | None => + match ov2 with + | Some v => + false + | None => + true + end + end. + +Check (eqb_polymorphic_binary_tree nat). +Check (eqb_polymorphic_binary_tree (option nat)). +Check (eqb_option (polymorphic_binary_tree nat)). + +(* +Definition eqb_binary_tree_of_optional_nats (t1 t2 : polymorphic_binary_tree (option nat)) : bool := +*) + +(* +Definition eqb_optional_binary_tree_of_nats (t1 t2 : option (polymorphic_binary_tree nat)) : bool := +*) + +(* +Definition eqb_optional_binary_tree_of_optional_nats (t1 t2 : option (polymorphic_binary_tree (option nat))) : bool := +*) + +(* +Definition eqb_binary_tree_of_optional_binary_tree_of_nats (t1 t2 : polymorphic_binary_tree (option (polymorphic_binary_tree nat))) : bool := +*) + +(* +Definition eqb_binary_tree_of_optional_binary_tree_of_optional_nats (t1 t2 : polymorphic_binary_tree (option (polymorphic_binary_tree (option nat)))) : bool := +*) + +(* ********** *) + +Inductive option' (V : Type) : Type := +| Some' : V -> option' V +| None' : option' V. + +Print option'. + +Set Implicit Arguments. + +Inductive option'' (V : Type) : Type := +| Some'' : V -> option'' V +| None'' : option'' V. + +Print option''. + +Check (Some 10, Some true). +Check (Some' nat 10, Some' bool true). +Check (Some'' 10, Some'' true). + +Check None. +Check None'. +Check None''. +Check (@None nat). +Check (@None' nat). +Check (@None'' nat). + +(* ********** *) + +(* end of week-01_polymorphism.v *) diff --git a/cs3234/labs/week-02_exercises.v b/cs3234/labs/week-02_exercises.v new file mode 100644 index 0000000..b78f9bb --- /dev/null +++ b/cs3234/labs/week-02_exercises.v @@ -0,0 +1,215 @@ +(* week-02_exercises.v *) +(* LPP 2024 - CS3234 2023-2024, Sem2 *) +(* Olivier Danvy *) +(* Version of 25 Jan 2024 *) + +(* ********** *) + +(* Exercises about types: *) + +Definition ta : forall A : Type, A -> A * A := + fun (A: Type) (a: A) => (a, a). + + +Definition tb : forall A B : Type, A -> B -> A * B := + fun (A B: Type) (a: A) (b: B) => (a, b). + +Definition tc : forall A B : Type, A -> B -> B * A := + fun (A B: Type) (a: A) (b: B) => (b, a). + + +Check (tt : unit). + +Definition td : forall (A : Type), (unit -> A) -> A := + fun (A : Type) (f: unit -> A) => f tt. + +Definition te : forall A B : Type, (A -> B) -> A -> B := + fun (A B : Type) (f: A -> B) (a: A) => f a. + +Definition tf : forall A B : Type, A -> (A -> B) -> B := + fun (A B : Type) (a: A) (f: A -> B) => f a. + + +Definition tg : forall A B C : Type, (A -> B -> C) -> A -> B -> C := + fun (A B C : Type) (f: A -> B -> C) (a: A) (b: B) => f a b. + +Definition th : forall A B C : Type, (A -> B -> C) -> B -> A -> C := + fun (A B C : Type) (f: A -> B -> C) (b: B) (a: A) => f a b. + +Definition ti : forall A B C D : Type, (A -> C) -> (B -> D) -> A -> B -> C * D := + fun (A B C D : Type) (f: A -> C) (g: B -> D) (a: A) (b: B) => (f a, g b). + + +Definition tj : forall A B C : Type, (A -> B) -> (B -> C) -> A -> C := + fun (A B C : Type) (f: A -> B) (g: B -> C) (a: A) => (g (f a)). + +Definition tk : forall A B : Type, A * B -> B * A := + fun (A B: Type) (p: A * B) => + match p with + | (a, b) => (b, a) + end. + +Definition tl : forall A B C : Type, (A * B -> C) -> A -> B -> C := + fun (A B C: Type) (f: A * B -> C) (a: A) (b: B) => f (a, b). + + +Definition tm : forall A B C : Type, (A -> B -> C) -> A * B -> C := + fun (A B C: Type) (f: A -> B -> C) (p: A * B) => + match p with + (a, b) => f a b + end. + + +Definition tn : forall A B C : Type, A * (B * C) -> (A * B) * C := + fun (A B C: Type) (p: A * (B * C)) => + match p with + (a, (b, c)) => ((a, b), c) + end. + +(* ********** *) + +(* Exercises about propositions: *) + +Proposition pa : + forall A : Prop, + A -> A /\ A. +Proof. + intros A H_A. + split. + - exact H_A. + - exact H_A. +Qed. + +Proposition pb : + forall A B : Prop, + A -> B -> A /\ B. +Proof. + intros A B H_A H_B. + split. + exact H_A. + exact H_B. +Qed. + +Proposition pc : + forall A B : Prop, + A -> B -> B /\ A. +Proof. + intros A B H_A H_B. + split. + exact H_B. + exact H_A. +Qed. + +Check tt. + +Proposition pd : + forall (A : Prop), + (unit -> A) -> A. +Proof. + intros A H_A. + exact (H_A tt). +Qed. + +Proposition pe : + forall A B : Prop, + (A -> B) -> A -> B. +Proof. + intros A B H_A_implies_B. + exact H_A_implies_B. + Restart. + intros A B H_A_implies_B H_A. + apply H_A_implies_B. + exact H_A. +Qed. + +Proposition pf : + forall A B : Prop, + A -> (A -> B) -> B. +Proof. + intros A B H_A H_A_implies_B. + exact (H_A_implies_B H_A). +Qed. + +Proposition pg : + forall A B C : Prop, + (A -> B -> C) -> A -> B -> C. +Proof. + intros A B C H_A_B_C. + exact H_A_B_C. +Qed. + +Proposition ph : + forall A B C : Prop, + (A -> B -> C) -> B -> A -> C. +Proof. + intros A B C H_A_B_C H_B H_A. + apply H_A_B_C. + - exact H_A. + - exact H_B. + Restart. + intros A B C H_ABC H_B H_A. + exact (H_ABC H_A H_B). +Qed. + +Proposition pi : + forall A B C D : Prop, + (A -> C) -> (B -> D) -> A -> B -> C /\ D. +Proof. + intros A B C D H_AC H_BD H_A H_B. + split. + - exact (H_AC H_A). + - exact (H_BD H_B). +Qed. + +Proposition pj : + forall A B C : Prop, + (A -> B) -> (B -> C) -> A -> C. +Proof. + intros A B C H_AB H_BC H_A. + apply H_BC. + apply H_AB. + exact H_A. +Qed. + +Proposition pk : + forall A B : Prop, + A /\ B -> B /\ A. +Proof. + intros A B [H_A H_B]. + split. + - exact H_B. + - exact H_A. +Qed. + +Proposition pl : + forall A B C : Prop, + (A /\ B -> C) -> A -> B -> C. +Proof. + intros A B C H_ABC H_A H_B. + apply H_ABC. + exact (conj H_A H_B). +Qed. + +Proposition pm : + forall A B C : Prop, + (A -> B -> C) -> A /\ B -> C. +Proof. + intros A B C H_ABC [H_A H_B]. + exact (H_ABC H_A H_B). +Qed. + +Proposition pn : + forall A B C : Prop, + (A /\ (B /\ C)) -> (A /\ B) /\ C. +Proof. + intros A B C [H_A [H_B H_C]]. + split. + - split. + * exact H_A. + * exact H_B. + - exact H_C. +Qed. + +(* ********** *) + +(* end of week-02_exercises.v *) diff --git a/cs3234/labs/week-02_formalizing-a-proof-in-tcpa.v b/cs3234/labs/week-02_formalizing-a-proof-in-tcpa.v new file mode 100644 index 0000000..c248f49 --- /dev/null +++ b/cs3234/labs/week-02_formalizing-a-proof-in-tcpa.v @@ -0,0 +1,325 @@ +(* week-02_formalizing-a-proof-in-tcpa.v *) +(* LPP 2024 - CS3234 2023-2024, Sem2 *) +(* Olivier Danvy *) +(* Version of 26 Jan 2024 with a correct definition of the specifications *) +(* was: *) +(* Version of 25 Jan 2024 *) + +(* ********** *) + +Require Import Arith Bool. + +(* ********** *) + +Definition lambda_dropped_specification_of_the_addition_function (add : nat -> nat -> nat) : Prop := + forall j : nat, + (add O j = j) + /\ + (forall i' ih : nat, + add i' j = ih -> + add (S i') j = S ih). + +Definition lambda_lifted_specification_of_the_addition_function (add : nat -> nat -> nat) : Prop := + (forall j : nat, + add O j = j) + /\ + (forall j i' ih : nat, + add i' j = ih -> + add (S i') j = S ih). + +(* ********** *) + +Lemma soundness_of_evenp (evenp : nat -> bool) : + forall n : nat, + evenp n = true -> + exists m : nat, + n = 2 * m. +Admitted. + +Lemma completeness_of_evenp (evenp : nat -> bool) : + forall n : nat, + (exists m : nat, + n = 2 * m) -> + evenp n = true. +Admitted. + +(* ********** *) + +(* Exercise 01 *) + +Proposition soundness_of_the_lambda_dropped_specification_of_the_addition_function : + forall add : nat -> nat -> nat, + lambda_dropped_specification_of_the_addition_function add -> + forall x y z : nat, + add x y = z -> + z = x + y. +Admitted. + +Proposition completeness_of_the_lambda_lifted_specification_of_the_addition_function : + forall add : nat -> nat -> nat, + lambda_lifted_specification_of_the_addition_function add -> + forall x y z : nat, + x + y = z -> + z = add x y. +Admitted. + +(* ********** *) + +(* Exercise 02 *) + + +Definition specification_of_negation (candidate : bool -> bool) : Prop := + (candidate true = false) /\ + (candidate false = true). + +Theorem soundness_of_the_specification_of_negation_with_respect_to_negb : + forall candidate: bool -> bool, + specification_of_negation candidate -> + forall b b': bool, + candidate b = b' -> + b' = negb b. +Admitted. + +Theorem completeness_of_the_specification_of_negation_with_respect_to_negb : + forall candidate: bool -> bool, + specification_of_negation candidate -> + forall b b': bool, + negb b = b' -> + candidate b = b'. +Admitted. + + +Definition negation (b : bool) : bool := + if b then false else true. + +Theorem negation_satisfies_the_specification_of_negation : + specification_of_negation negation. + Admitted. + +Theorem soundness_of_negation_with_respect_to_negb : + forall b b' : bool, + negation b = b' -> + b' = negb b. +Admitted. + +Theorem completeness_of_negation_with_respect_to_negb : + forall b b' : bool, + negb b = b' -> + b' = negation b. +Admitted. + +Theorem soundness_of_negb_with_respect_to_negation : + forall b b' : bool, + negb b = b' -> + b' = negation b. +Admitted. + +Theorem completeness_of_negb_with_respect_to_negation : + forall b b' : bool, + negation b = b' -> + b' = negb b. +Admitted. +(* ********** *) + +Search (_ + 0 = _). + +Check Nat.add_0_r. + +Proposition first_formal_proof : + forall n : nat, + n + 0 = 0 + n. +Proof. + intro n. + Check (Nat.add_0_r n). + rewrite -> (Nat.add_0_r n). + Check (Nat.add_0_l n). + rewrite -> (Nat.add_0_l n). + reflexivity. +Qed. + +Check first_formal_proof. + +Proposition first_formal_proof' : + forall n : nat, + n + 0 = 0 + n. +Proof. + intro n. + rewrite -> (Nat.add_0_l n). + rewrite -> (Nat.add_0_r n). + reflexivity. +Qed. + +Proposition first_formal_proof'' : + forall n : nat, + n + 0 = 0 + n. +Proof. + intro n. + rewrite -> (Nat.add_0_r n). + rewrite -> (Nat.add_0_l n). + reflexivity. + + Restart. + + intro n. + rewrite -> (Nat.add_0_l n). + rewrite -> (Nat.add_0_r n). + reflexivity. +Qed. + +Proposition first_formal_proof''' : + forall n : nat, + n + 0 = 0 + n. +Proof. + intro n. + Check (Nat.add_comm n 0). + exact (Nat.add_comm n 0). + + Restart. + + intro n. + Check (Nat.add_comm 0 n). + symmetry. + exact (Nat.add_comm 0 n). +Qed. + +(* ********** *) + + +Search (_ + _ = _ + _). +Proposition first_formal_proof'''' : + forall n : nat, + n + 0 = 0 + n. +Proof. + intro n. + exact (Nat.add_comm n 0). + + Restart. + intro n. + symmetry. + exact (Nat.add_comm 0 n). + Qed. +(* +Nat.add_comm: forall n m : nat, n + m = m + n +Nat.add_assoc: forall n m p : nat, n + (m + p) = n + m + p +*) + +Check (Nat.add_comm 2 3). + +Proposition second_formal_proof: + forall x y z : nat, + x + (y + z) = y + (x + z). +Proof. + intro x. + intro y. + intro z. + Search (_ + (_ + _)). + Check (Nat.add_assoc x y z). + + rewrite -> (Nat.add_assoc x y z). + Check Nat.add_comm. + rewrite -> (Nat.add_comm x y). + rewrite <- (Nat.add_assoc). + reflexivity. + Restart. + intros x y z. + rewrite -> (Nat.add_assoc x y z). + rewrite -> (Nat.add_comm x y). + rewrite <- (Nat.add_assoc y x z). + reflexivity. +Qed. + + + +(* ********** *) + +Proposition third_formal_proof: + forall n : nat, + n + 0 + 0 = 0 + 0 + n. +Proof. + intro n. + rewrite -> (Nat.add_0_r n). + rewrite -> (Nat.add_0_r n). + + Check (Nat.add_0_l 0). + rewrite -> (Nat.add_0_l 0). + rewrite -> (Nat.add_0_l n). + reflexivity. + Restart. + intro n. + rewrite -> (Nat.add_0_r n). + rewrite -> (Nat.add_0_r n). + rewrite -> (Nat.add_0_l 0). + exact (Nat.add_0_l n). + + Restart. + intro n. + Check (first_formal_proof (n + 0)). + rewrite -> (first_formal_proof (n + 0)). + Check (first_formal_proof n). + rewrite -> (first_formal_proof n). + exact (Nat.add_assoc 0 0 n). + + Restart. + intro n. + Check (Nat.add_0_l 0). + rewrite -> (Nat.add_0_l 0). + rewrite -> (Nat.add_0_r n). + Check first_formal_proof. + exact (first_formal_proof n). + Qed. + +(* ********** *) +(* Exercise 3 *) +Proposition foo : + forall n1 n2 n3 n4 : nat, + n1 + (n2 + (n3 + n4)) = ((n1 + n2) + n3) + n4. +Proof. + intros a b c d. + Search (_ + (_ + _) = _ + _ + _). + rewrite -> (Nat.add_assoc a b (c + d)). + Check Nat.add_assoc. + rewrite -> (Nat.add_assoc (a + b) c d). + reflexivity. + Qed. +(* ********** *) +(* Exercise 4 *) +(* ********** *) +(* Exercise 5 *) +Proposition binomial_expansion_2_warmup : + forall x y : nat, + (x + y) * (x + y) = x * x + x * y + x * y + y * y. +Proof. + intros x y. + Search (_ * (_ + _) = _). + Check Nat.mul_add_distr_l. + Check Nat.mul_add_distr_r. + rewrite -> (Nat.mul_add_distr_l (x + y) x y). + rewrite -> (Nat.mul_add_distr_r x y x ). + rewrite -> (Nat.mul_comm y x). + rewrite -> (Nat.mul_add_distr_r x y y ). + Check Nat.add_assoc. + rewrite -> (Nat.add_assoc (x * x + x * y) (x * y) (y * y)). + reflexivity. + Qed. + +Proposition binomial_expansion_2 : + forall x y : nat, + (x + y) * (x + y) = x * x + 2 * (x * y) + y * y. +Proof. + intros x y. + + Check (Nat.mul_succ_l 1 (x * y)). + rewrite -> (Nat.mul_succ_l 1 (x * y)). + Search (1 * _). + rewrite -> (Nat.mul_1_l (x * y)). + rewrite -> (Nat.add_assoc (x * x) (x * y) (x * y)). + + exact (binomial_expansion_2_warmup x y). + + Qed. + +(* ********** *) + + + +(* end of week-02_formalizing-a-proof-in-tcpa.v *) diff --git a/cs3234/labs/week-02_proving-logical-properties.v b/cs3234/labs/week-02_proving-logical-properties.v new file mode 100644 index 0000000..dc1d49c --- /dev/null +++ b/cs3234/labs/week-02_proving-logical-properties.v @@ -0,0 +1,539 @@ +(* week-02_proving-logical-properties.v *) +(* LPP 2024 - CS3234 2023-2024, Sem2 *) +(* Olivier Danvy *) +(* Version of 25 Jan 2024 *) + +(* ********** *) + +Lemma identity : + forall A : Prop, + A -> A. +Proof. + intro A. + intro H_A. + exact H_A. +Qed. + +(* ********** *) + +Lemma proving_a_conjunction : + forall A B : Prop, + A -> B -> A /\ B. +Proof. + intros A B H_A H_B. + split. + + exact H_A. + + exact H_B. + + Restart. + + intros A B H_A H_B. + split. + { exact H_A. } + { exact H_B. } + + Restart. + + intros A B H_A H_B. + split. + - exact H_A. + + - exact H_B. + + Restart. + + intros A B H_A H_B. + Check (conj H_A H_B). + exact (conj H_A H_B). +Qed. + +(* ********** *) + +Lemma proving_a_ternary_conjunction : + forall A B C : Prop, + A -> B -> C -> A /\ B /\ C. +Proof. + intros A B C. + intros H_A H_B H_C. + split. + - exact H_A. + - split. + + exact H_B. + + exact H_C. + + Restart. + + intros A B C. + intros H_A H_B H_C. + exact (conj H_A (conj H_B H_C)). + + Restart. + intros A B C. + intros H_A H_B H_C. + split. + { exact H_A. } + split. + { exact H_B. } + exact H_C. + +Qed. +(* ********** *) + +Lemma example_for_Anton : + forall A B C D : Prop, + A /\ B /\ C /\ D. +Proof. + intros A B C D. + split. + - admit. + - split. + + admit. + + split. + * admit. + * admit. + + Restart. + + intros A B C D. + split. + { admit. } + { split. + { admit. } + { split. + { admit. } + { admit. } } } + + Restart. + + intros A B C D. + split. + { admit. } + split. + { admit. } + split. + { admit. } + admit. +Abort. + +(* ********** *) + +Lemma proving_a_disjunction : + forall A B : Prop, + A -> B -> A \/ B. +Proof. + intros A B H_A H_B. + left. + exact H_A. + + Restart. + + intros A B H_A H_B. + right. + exact H_B. +Qed. + +(* ********** *) + +(* Exercise 06 *) + +Lemma conjunction_is_commutative: + forall A B : Prop, + A /\ B <-> B /\ A. +Proof. + intros A B. + split. + - intros [H_A H_B]. + exact (conj H_B H_A). + - intros [H_B H_A]. + exact (conj H_A H_B). + Qed. + +Lemma conjunction_is_commutative_aux : + forall A B : Prop, + A /\ B -> B /\ A. +Proof. + intros A B [H_A H_B]. + exact (conj H_B H_A). +Qed. + +Lemma conjunction_is_commutative_revisited : + forall A B : Prop, + A /\ B <-> B /\ A. +Proof. + intros A B. + split. + + - exact (conjunction_is_commutative_aux A B). + + - exact (conjunction_is_commutative_aux B A). +Qed. + +(* ********** *) + +(* Exercise 07 *) + +Lemma conjunction_is_associative_aux: + forall A B C : Prop, + A /\ (B /\ C) -> (A /\ B) /\ C. +Proof. + intros A B C. + intros [H_A [H_B H_C]]. + exact (conj (conj H_A H_B) H_C). + Qed. + +Lemma conjunction_is_associative : + forall A B C : Prop, + A /\ (B /\ C) <-> (A /\ B) /\ C. +Proof. + intros A B C. + split. + - intros [H_A [H_B H_C]]. + Check (conj (conj H_A H_B) H_C). + exact (conj (conj H_A H_B) H_C). + - intros [[H_A H_B] H_C]. + exact (conj H_A (conj H_B H_C)). + + Restart. + intros A B C. + split. + - intros [H_A [H_B H_C]]. + split. + * split. + exact H_A. + exact H_B. + * exact H_C. + - intros [[H_A H_B] H_C]. + split. + exact H_A. + * split. + exact H_B. + exact H_C. +Qed. + + +(* ********** *) + +(* Exercise 08 *) +Lemma disjunction_is_commutative_aux : + forall A B : Prop, + A \/ B -> B \/ A. +Proof. + intros A B. + intros [H_A | H_B]. + right. + exact H_A. + left. + exact H_B. +Qed. + + +Lemma disjunction_is_commutative : + forall A B : Prop, + A \/ B <-> B \/ A. +Proof. + intros A B. + split. + - intros [H_A | H_B]. + right. + exact H_A. + left. + exact H_B. + - intros [H_B | H_A]. + right. + exact H_B. + left. + exact H_A. + Restart. + intros A B. + split. + - exact (disjunction_is_commutative_aux A B). + - exact (disjunction_is_commutative_aux B A). +Qed. + +(* ********** *) + +(* Exercise 09 *) + +Lemma disjunction_is_associative : + forall A B C : Prop, + A \/ (B \/ C) <-> (A \/ B) \/ C. +Proof. + intros A B C. + split. + - intros [H_A | [H_B | H_C]]. + left. + left. + exact H_A. + left. + right. + exact H_B. + right. + exact H_C. + - intros [[H_A | H_B] | H_C]. + left. + exact H_A. + right. + left. + exact H_B. + right. + right. + exact H_C. +Qed. + +(* ********** *) + +(* Exercise 10 *) + +(* Prove whether disjunction distribute over conjunction on the left and on the right. *) + +Proposition disjunction_distributes_over_conjunction_on_the_left : + forall A B C : Prop, + A \/ (B /\ C) <-> (A \/ B) /\ (A \/ C). +Proof. + intros A B C. + split. + - intros [H_A | [H_B H_C]]. + + + split. + * left. + exact H_A. + * left. + exact H_A. + + split. + * right. + exact H_B. + * right. + exact H_C. + + - intros [[H_A | H_B] [H_A' | H_C]]. + + left. + exact H_A. + + left. + exact H_A. + + left. + exact H_A'. + + right. + exact (conj H_B H_C). + Qed. + +Proposition disjunction_distributes_over_conjunction_on_the_right : + forall A B C : Prop, + (B /\ C) \/ A <-> (B \/ A) /\ (C \/ A). +Proof. + intros A B C. + split. + - intros [[H_B H_C] | H_A]. + + split. + * left. + exact H_B. + * left. + exact H_C. + + split. + * right. + exact H_A. + * right. + exact H_A. + - intros [[H_B | H_A] [H_C | H_A']]. + + left. + exact (conj H_B H_C). + + right. + exact H_A'. + + right. + exact H_A. + + right. + exact H_A. +Qed. + + + +(* ********** *) + +(* Exercise 11 *) + +(* +Does conjunction distribute over disjunction on the left? +And what about on the right? +*) + +(* ********** *) + +Proposition modus_ponens : + forall A B : Prop, + A -> (A -> B) -> B. +Proof. + intros A B. + intros H_A H_A_implies_B. + Check (H_A_implies_B H_A). + exact (H_A_implies_B H_A). + + Restart. + + intros A B. + intros H_A H_A_implies_B. + apply H_A_implies_B. + exact H_A. +Qed. + +(* ********** *) + +(* Exercise 12 *) + +Proposition following : + forall A B : Prop, + (A -> B) -> A -> B. +Proof. + intros A B. + intros H_A_implies_B. + intros H_A. + exact (H_A_implies_B H_A). + Restart. + intros A B. + intros H_A_implies_B. + apply H_A_implies_B. +Qed. + + +(* ********** *) + +Proposition modus_tollens : + forall A B : Prop, + ~B -> (A -> B) -> ~A. +Proof. + intros A B. + unfold not. + intros H_B_implies_False H_A_implies_B H_A. + apply H_B_implies_False. + apply H_A_implies_B. + exact H_A. + + Restart. + + intros A B. + unfold not. + intros H_B_implies_False H_A_implies_B H_A. + Check (H_A_implies_B H_A). + Check (H_B_implies_False (H_A_implies_B H_A)). + exact (H_B_implies_False (H_A_implies_B H_A)). + + Restart. + + intros A B. + unfold not. + intros H_B_implies_False H_A_implies_B H_A. + Check (modus_ponens A B). + Check (modus_ponens A B H_A). + Check (modus_ponens A B H_A H_A_implies_B). + Check (H_B_implies_False (modus_ponens A B H_A H_A_implies_B)). + exact (H_B_implies_False (modus_ponens A B H_A H_A_implies_B)). +Qed. + +(* ********** *) + +(* Exercise 13 *) + +Proposition implication_distributes_over_conjunction_on_the_left : + forall A B C : Prop, + (A -> B /\ C) <-> ((A -> B) /\ (A -> C)). +Proof. + intros A B C. + split. + + - intros H_A_implies_B_and_C. + split. + + * intro H_A. + Check (H_A_implies_B_and_C H_A). + destruct (H_A_implies_B_and_C H_A) as [H_B _]. + exact H_B. + + * intro H_A. + destruct (H_A_implies_B_and_C H_A) as [_ H_C]. + exact H_C. + + - intros [H_A_implies_B H_A_implies_C] H_A. + Check (H_A_implies_B H_A). + Check (H_A_implies_C H_A). + Check (conj (H_A_implies_B H_A) (H_A_implies_C H_A)). + exact (conj (H_A_implies_B H_A) (H_A_implies_C H_A)). +Qed. + +(* ********** *) + +(* Exercise 14 *) + +Proposition implication_distributes_over_disjunction_on_the_right_and_with_a_twist : + forall A B C : Prop, + ((A \/ B) -> C) <-> ((A -> C) /\ (B -> C)). +Proof. + intros A B C. + split. + + - intros H_A_or_B_implies_C. + split. + + + intro H_A. + apply H_A_or_B_implies_C. + left. + exact H_A. + + + intro H_B. + apply H_A_or_B_implies_C. + right. + exact H_B. + + - intros [H_A_implies_C H_B_implies_C] [H_A | H_B]. + + + Check (H_A_implies_C H_A). + exact (H_A_implies_C H_A). + + + exact (H_B_implies_C H_B). +Qed. + +(* ********** *) + +(* Exercise 15 *) + +Proposition contrapositive_of_implication : + forall A B : Prop, + (A -> B) -> ~B -> ~A. +Proof. + intros A B. + intros H_A_implies_B H_not_B. + Check (modus_tollens A B H_not_B H_A_implies_B). + exact (modus_tollens A B H_not_B H_A_implies_B). +Qed. + +(* ********** *) + +(* Exercise 16 *) + +Proposition contrapositive_of_contrapositive_of_implication : + forall A B : Prop, + (~B -> ~A) -> ~~A -> ~~B. +Proof. + intros A B. + Check (contrapositive_of_implication (not B) (not A)). + exact (contrapositive_of_implication (not B) (not A)). +Qed. + +(* ********** *) + +(* Exercise 17 *) + +Proposition double_negation : + forall A : Prop, + A -> ~~A. +Proof. + intros A. + intros H_A. + unfold not. + intros H_A_implies_false. + apply H_A_implies_false. + exact H_A. +Qed. + +(* ********** *) + +(* end of week-02_proving-logical-properties.v *) diff --git a/cs3234/labs/week-02_the-intro-tactic.v b/cs3234/labs/week-02_the-intro-tactic.v new file mode 100644 index 0000000..c92203b --- /dev/null +++ b/cs3234/labs/week-02_the-intro-tactic.v @@ -0,0 +1,110 @@ +(* week-02_the-intro-tactic.v *) +(* LPP 2023 - CS3234 2023-2024, Sem2 *) +(* Olivier Danvy *) +(* Version of 25 Jan 2024 *) + +(* ********** *) + +Lemma a_proposition_implies_itself : + forall A : Prop, + A -> A. +Proof. + intro A. + intro H_A. + exact H_A. + + Restart. + + intro rose. + intro H_rose. + exact H_rose. +Qed. + +(* ********** *) + +Lemma the_following_example : + forall A B C : Prop, + A -> + B -> + C -> + forall i j : nat, + A /\ B /\ C /\ i = i /\ j = j. +Proof. + intros A B C. + intros H_A H_B H_C. + intros i j. + split. + exact H_A. + split. + exact H_B. + split. + exact H_C. + split. + reflexivity. + reflexivity. +Qed. + +(* ********** *) + +Lemma a_pair_of_propositions_implies_the_left_one : + forall A B : Prop, + A /\ B -> A. +Proof. + intros A B. + intro H_A_and_B. + destruct H_A_and_B. + exact H. + + Restart. + + intros A B. + intro H_A_and_B. + destruct H_A_and_B as [H_A H_B]. + exact H_A. + + Restart. + + intros A B. + intros [H_A H_B]. + exact H_A. +Qed. + +(* ********** *) + +Lemma disjunction_is_commutative : + forall A B : Prop, + A \/ B -> B \/ A. +Proof. + intros A B. + intros [H_A | H_B]. + + - right. + exact H_A. + + - left. + exact H_B. +Qed. + +(* ********** *) + +Lemma about_nested_conjunctions : + forall A B C D : Prop, + (A /\ B) /\ (C /\ D) -> (D /\ A) /\ (B /\ C). +Proof. + intros A B C D. + intros [[H_A H_B] [H_C H_D]]. + Check (conj (conj H_D H_A) (conj H_B H_C)). + exact (conj (conj H_D H_A) (conj H_B H_C)). +Qed. + +Lemma about_nested_conjunctions_and_disjunctions : + forall A B C D E F : Prop, + (A \/ B) /\ (C \/ (D /\ E)) -> F. +Proof. + intros A B C D E F. + intros [[H_A | H_B] [H_C | [H_D H_E]]]. +Abort. + +(* ********** *) + +(* end of week-02_the-intro-tactic.v *) diff --git a/cs3234/labs/week-02_the-revert-tactic.v b/cs3234/labs/week-02_the-revert-tactic.v new file mode 100644 index 0000000..ab44def --- /dev/null +++ b/cs3234/labs/week-02_the-revert-tactic.v @@ -0,0 +1,67 @@ +(* week-02_the-revert-tactic.v *) +(* LPP 2024 - CS3234 2023-2024, Sem2 *) +(* Olivier Danvy *) +(* Version of 28 Jan 2024, with an instance of revert with several arguments *) +(* was: *) +(* Version of 25 Jan 2024 *) + +(* ********** *) + +Lemma a_proposition_implies_itself : + forall A : Prop, + A -> A. +Proof. + intro A. + intro H_A. + exact H_A. + + Restart. + + intro A. + intro H_A. + revert H_A. (* <-- *) + revert A. (* <-- *) + intros A H_A. + exact H_A. +Qed. + +(* ********** *) + +Lemma swapping_the_order_of_quantifiers : + forall A B : Prop, + (A -> B -> A /\ B) -> B -> A -> A /\ B. +Proof. + intros A B H_implication H_B H_A. + exact (H_implication H_A H_B). + + Restart. + + intros A B H_implication H_B H_A. + revert H_B. + revert H_A. + exact H_implication. + + Restart. + + intros A B H_implication H_B H_A. + revert H_B. + revert H_A. + revert H_implication. + exact (a_proposition_implies_itself (A -> B -> A /\ B)). + + Restart. + + intros A B H_implication H_B H_A. + revert H_A H_B. + exact H_implication. + + Restart. + + intros A B H_implication H_B H_A. + revert H_implication H_A H_B. + exact (a_proposition_implies_itself (A -> B -> A /\ B)). +Qed. + +(* ********** *) + +(* end of week-02_the-revert-tactic.v *)