[coq] add de-morgan laws

coq/README.org

@@ -1 +1,8 @@
- - sumn.v: Sum of first n natural numbers, their squares and cubes.
+#+TITLE: Coq
+
+ - [[./sumn.v]]: Sum of first n natural numbers, their squares and cubes.
+ - [[./de-morgan.v]]: de-Morgan's laws
+ - [[./eqns.v]]: A 'hello world' using the 'equations' plugin
+ - [[./cpdt/]]: stuff from the book CPDT
+ - [[./sf/]]: stuff from /Software foundations/
+

coq/cpdt/exercises.v

@@ -0,0 +1,82 @@
+(* http://adam.chlipala.net/cpdt/ex/exercises.pdf *)
+
+
+(* ** 0.1 *)
+
+Inductive truth : Type := Yes | No | Maybe.
+
+Definition tnot (a: truth) : truth :=
+  match a with
+  | Yes => No
+  | No => Yes
+  | Maybe => Maybe
+  end.
+
+Definition tor (a b: truth) : truth :=
+  match a, b with
+  | Yes, _ => Yes
+  | _, Yes => Yes
+  | Maybe, _ => Maybe
+  | _, Maybe => Maybe
+  | No, No => No
+  end.
+
+Definition tand (a b: truth) : truth :=
+  match a, b with
+  | Yes, Yes => Yes
+  | No, _ => No
+  | _, No => No
+  | Maybe, _ => Maybe
+  | _, Maybe => Maybe
+  end.
+
+(* [tand] is commutative *)
+Theorem tand_comm: forall a b c:truth,
+  tand (tand a b) c = tand a (tand b c).
+Proof.
+  intros a b c.
+  induction a; induction b; induction c; trivial.
+Qed.
+
+(* [tand] distributes over [tor] *)
+Theorem tand_distr: forall a b c:truth,
+  tand a (tor b c) = tor (tand a b) (tand a c).
+Proof.
+  intros a b c.
+  induction a; induction b; induction c; trivial.
+Qed.
+
+(* ** 0.2 *)
+
+Require List.
+
+Inductive slist {A:Type}: Type :=
+| SNil: slist
+| SCons: A -> slist
+| SApp: slist -> slist -> slist.
+Arguments slist: clear implicits.
+
+(*
+Definition sapp {A:Type} (a b:slist A): slist A :=
+  match a, b with
+  | SNil, _ => b
+  | _, SNil => a
+  | _, _ => SCons a b
+  end.
+*)
+
+Fixpoint flatten {A:Type} (a:slist A) : list A :=
+  match a with
+  | SNil => List.nil
+  | SCons x => List.cons x List.nil
+  | SApp x y => List.app (flatten x) (flatten y)
+  end.
+
+Theorem flatten_app_distr {A:Type}: forall a b:slist A,
+  flatten (SApp a b) = List.app (flatten a) (flatten b).
+Proof.
+  intros a b.
+  induction a; induction b; trivial.
+Qed.
+
+(* ** 0.3 *)

coq/de-morgan.v

@@ -0,0 +1,92 @@
+Theorem dM1: forall A B:Prop,
+  ~(or A B) -> and (~A) (~B).
+Proof.
+  intros A B H.
+  split.
+  - intro a.
+    apply (H (or_introl a)).
+  - intro b.
+    exact (H (or_intror b)).
+Qed.
+
+Theorem dM1r: forall A B:Prop,
+  and (~A) (~B) -> ~(or A B).
+Proof.
+  intros A B.
+  intro nA_and_nB.
+  intro AorB.
+  unfold not in nA_and_nB.
+  destruct AorB.
+  - destruct nA_and_nB.
+    exact (H0 H).
+  - destruct nA_and_nB.
+    exact (H1 H).
+Qed.
+
+Theorem dM2r: forall A B:Prop,
+  or (~A) (~B) -> ~(and A B).
+Proof.
+  intros A B H.
+  unfold not.
+  intro A_and_B.
+  destruct H.
+  - unfold not in H.
+    destruct A_and_B.
+    exact (H H0).
+  - destruct A_and_B.
+    unfold not in H.
+    exact (H H1).
+Qed.
+
+(* The unprovable de-Morgan law is equivalent ot LEM *)
+(* https://github.com/coq-community/coq-art/blob/master/ch5_everydays_logic/SRC/class.v#L53 *)
+
+Definition lem := forall P:Prop, P\/~P.
+Definition deM := forall P Q:Prop, ~(~P/\~Q)->P\/Q.
+
+Lemma foo : deM -> lem.
+Proof.
+  unfold lem.
+  intros H P.
+  apply H. (* P=P, Q=~P *) (* New goal: ~(~P /\ ~~P) *)
+  intros [HnP HnnP].
+  contradiction.
+Qed.
+Lemma foo_r : lem -> deM.
+Proof.
+  unfold lem.
+  intro H.
+  unfold deM.
+  intros P Q.
+  intro H2.
+  (*
+  intros [HnP HnQ].
+  intros H P.
+  apply H. (* P=P, Q=~P *) (* New goal: ~(~P /\ ~~P) *)
+  intros [HnP HnnP].
+  contradiction.
+   *)
+Abort.
+
+Theorem foo23:
+  let deM := forall A B:Prop, ~(~A /\ ~B) -> (A \/ B) in
+  let lem := forall A:Prop, A \/ ~A in
+  deM -> lem.
+Proof.
+  intros dem lem.
+  subst lem.
+  intro dm.
+  intro A.
+  apply dm.
+  intros [HnP HnnP].
+  contradiction.
+Qed.
+  
+Theorem foo32:
+  let deM := forall A B:Prop, ~(~A /\ ~B) -> (A \/ B) in
+  let lem := forall A:Prop, A \/ ~A in
+  lem -> deM.
+Proof.
+  intros lem dem.
+  subst dem.
+  intro dm.

coq/eqns.v

@@ -0,0 +1,23 @@
+From Equations Require Import Equations.
+Require Import List ZArith Lia.
+Import ListNotations.
+
+Equations neg (b : bool) : bool :=
+neg true := false;
+neg false := true.
+Compute neg true.   (* false : bool *)
+Compute neg false.  (* true : bool *)
+
+Equations bin (n : nat) : list bool by wf n lt :=
+bin O := List.nil;
+bin n := (if (Nat.eqb (Nat.modulo n 2) 0) then false else true)  :: bin (Nat.div n 2).
+Next Obligation.
+  change (S n0 / 2 < S n0).
+  apply Nat.div_lt; lia.
+Qed.
+Compute bin 11.
+(*
+= [true; true; false; true]
+     : list bool
+*)
+

coq/mult.v

@@ -0,0 +1,122 @@
+Lemma add_n_0: forall n:nat, n+0 = n.
+Proof.
+  intro n.
+  induction n.
+  - reflexivity.
+  - simpl.
+    rewrite IHn.
+    reflexivity.
+Qed.
+
+Lemma add_nSm: forall n m:nat,
+  n + S m = S (n + m).
+Proof.
+  intros n m.
+  induction n.
+  - reflexivity.
+  - simpl.
+    rewrite <- IHn.
+    reflexivity.
+Qed.
+
+Theorem plus_comm : forall a b:nat,
+  a + b = b + a.
+Proof.
+  intros a b.
+  induction a.
+  - rewrite add_n_0.
+    reflexivity.
+  - simpl.
+    rewrite add_nSm.
+    rewrite <- IHa.
+    reflexivity.
+Qed.
+
+Theorem plus_assoc : forall a b c:nat,
+  a + (b + c) = (a + b) + c.
+Proof.
+  intros a b c.
+  induction a.
+  - reflexivity.
+  - simpl.
+    rewrite IHa.
+    reflexivity.
+Qed.
+
+Lemma mult_n_0: forall n:nat, n*0 = 0.
+Proof.
+  intros n.
+  induction n.
+  - reflexivity.
+  - simpl.
+    rewrite IHn.
+    reflexivity.
+Qed.
+
+Lemma mult_nSm: forall n m:nat,
+  n * S m = n + (n * m).
+Proof.
+  intros n m.
+  induction n.
+  - reflexivity.
+  - simpl.
+    rewrite IHn.
+    SearchRewrite ((_ + _) + _).
+    rewrite plus_assoc.
+    rewrite (plus_comm m n).
+    rewrite <- plus_assoc.
+    reflexivity.
+Qed.
+
+Theorem mult_comm: forall a b:nat,
+  a * b = b * a.
+Proof.
+  intros a b.
+  induction a.
+  - rewrite mult_n_0.
+    reflexivity.
+  - simpl.
+    rewrite mult_nSm.
+    rewrite <- IHa.
+    reflexivity.
+Qed.
+
+Theorem mult_distr_l : forall a b c:nat,
+  a * (b + c) = (a * b) + (a * c).
+Proof.
+  intros a b c.
+  induction a.
+  - reflexivity.
+  - simpl.
+    rewrite IHa.
+    rewrite plus_assoc.
+    rewrite plus_assoc.
+    rewrite <- (plus_assoc b c (a*b)).
+    rewrite (plus_comm c (a*b)).
+    rewrite plus_assoc.
+    reflexivity.
+Qed.
+
+Theorem mult_distr_r : forall a b c:nat,
+  (a + b) * c = (a * c) + (b * c).
+Proof.
+  intros a b c.
+  induction a.
+  - reflexivity.
+  - simpl.
+    rewrite <- (plus_assoc c (a*c) (b*c)).
+    rewrite <- IHa.
+    reflexivity.
+Qed.
+
+Theorem mult_assoc : forall a b c:nat,
+  a * (b * c) = (a * b) * c.
+Proof.
+  intros a b c.
+  induction a.
+  - reflexivity.
+  - simpl.
+    rewrite IHa.
+    rewrite mult_distr_r.
+    reflexivity.
+Qed.