~pmikkelsen/software-foundations

37fce3f72ff39db57eba8f51281abbd8c9fbb4bd — Peter Mikkelsen 1 year, 1 month ago 5aebf82
Progress on logic
1 files changed, 623 insertions(+), 0 deletions(-)

M vol1/Logic.v
M vol1/Logic.v => vol1/Logic.v +623 -0
@@ 0,0 1,623 @@
From LF Require Export Tactics.

Theorem plus_2_2_is_4:
  2 + 2 = 4.
Proof. reflexivity. Qed.

Definition plus_claim : Prop := 2 + 2 = 4.

Theorem plus_claim_is_true : plus_claim.
Proof. reflexivity. Qed.

Definition is_three (n : nat) : Prop :=
  n = 3.

Definition injective {A B} (f : A -> B) :=
  forall x y : A,
  f x = f y ->
  x = y.

Lemma succ_inj : injective S.
Proof.
  intros n m H.
  injection H as H. apply H.
Qed.

Example and_example:
  3 + 4 = 7 /\ 2 * 2 = 4.
Proof.
  split.
  - reflexivity.
  - reflexivity.
Qed.

Lemma and_intro : forall A B : Prop,
  A -> B -> A /\ B.
Proof.
  intros A B HA HB.
  split.
  - apply HA.
  - apply HB.
Qed.

Example and_example': 3 + 4 = 7 /\ 2 * 2 = 4.
Proof.
  apply and_intro.
  - reflexivity.
  - reflexivity.
Qed.

Example and_exercise :
  forall n m : nat,
  n + m = 0 ->
  n = 0 /\ m = 0.
Proof.
  intros.
  split.
  - destruct n.
    + reflexivity.
    + discriminate H.
  - destruct m.
    + reflexivity.
    + rewrite <- plus_n_Sm in H.
      discriminate H.
Qed.

Lemma and_example2:
  forall n m : nat,
  n = 0 /\ m = 0 ->
  n + m = 0.
Proof.
  intros.
  destruct H as [HA HB].
  rewrite HA, HB.
  reflexivity.
Qed.

Lemma and_example2' :
  forall n m : nat,
  n = 0 /\ m = 0 ->
  n + m = 0.
Proof.
  intros n m [Hn Hm].
  rewrite Hn, Hm.
  reflexivity.
Qed.

Lemma and_example2'' :
  forall n m : nat,
  n = 0 ->
  m = 0 ->
  n + m = 0.
Proof.
  intros n m Hn Hm.
  rewrite Hn, Hm.
  reflexivity.
Qed.

Lemma and_example3:
  forall n m : nat,
  n + m = 0 ->
  n * m = 0.
Proof.
  intros n m H.
  apply and_exercise in H.
  destruct H as [Hn Hm].
  rewrite Hn. reflexivity.
Qed.

Lemma proj1 : forall P Q : Prop,
  P /\ Q -> P.
Proof.
  intros P Q HPQ.
  destruct HPQ as [HP _].
  apply HP.
Qed.

Lemma proj2 : forall P Q : Prop,
  P /\ Q -> Q.
Proof.
  intros P Q HPQ.
  destruct HPQ as [_ HQ].
  apply HQ.
Qed.

Theorem and_commut : forall P Q : Prop,
  P /\ Q -> Q /\ P.
Proof.
  intros P Q [HP HQ].
  split.
  - apply HQ.
  - apply HP.
Qed.

Theorem and_assoc: forall P Q R : Prop,
  P /\ (Q /\ R) ->
  (P /\ Q) /\ R.
Proof.
  intros P Q R [HP [HQ HR]].
  split.
  - split.
    + apply HP.
    + apply HQ.
  - apply HR.
Qed.

Lemma factor_is_O:
  forall n m : nat,
  n = 0 \/ m = 0 ->
  n * m = 0.
Proof.
  intros n m [Hn | Hm].
  - rewrite Hn. reflexivity.
  - rewrite Hm. rewrite <- mult_n_O. reflexivity.
Qed.

Lemma or_intro_l : forall A B : Prop,
  A -> A \/ B.
Proof.
  intros A B HA.
  left.
  apply HA.
Qed.

Lemma zero_or_succ:
  forall n : nat,
  n = 0 \/ n = S (pred n).
Proof.
  destruct n.
  - left. reflexivity.
  - right. reflexivity.
Qed.

Lemma mult_is_O:
  forall n m,
  n * m = 0 ->
  n = 0 \/ m = 0.
Proof.
  intros.
  destruct n.
  - left. reflexivity.
  - right. destruct m.
    + reflexivity.
    + discriminate H.
Qed.

Theorem or_commut : forall P Q : Prop,
  P \/ Q -> Q \/ P.
Proof.
  intros P Q [HP | HQ].
  - right. apply HP.
  - left. apply HQ.
Qed.

Module NotPlayground.
Definition not (P:Prop) := P -> False.
Notation "~ x" := (not x) : type_scope.
End NotPlayground.

Theorem ex_falso_quodlibet : forall (P : Prop),
  False -> P.
Proof.
  intros.
  destruct H.
Qed.

Theorem not_implies_our_not : forall (P : Prop),
  ~ P -> (forall Q : Prop, P -> Q).
Proof.
  intros P NP Q HP.
  apply NP in HP.
  destruct HP.
Qed.

Theorem zero_not_one : 0 <> 1.
Proof.
  intros H.
  discriminate H.
Qed.

Theorem not_False : ~ False.
Proof.
  intros H.
  apply H.
Qed.

Theorem contradiction_implies_anything : forall P Q : Prop,
  (P /\ ~P) -> Q.
Proof.
  intros P Q [HP HNP].
  apply HNP in HP.
  destruct HP.
Qed.

Theorem double_neg : forall P : Prop,
  P -> ~~P.
Proof.
  intros P H.
  unfold not.
  intros G.
  apply G.
  apply H.
Qed.

Theorem contrapositive : forall (P Q : Prop),
  (P -> Q) -> (~Q -> ~P).
Proof.
  intros P Q H.
  unfold not.
  intros G HP.
  apply G, H, HP.
Qed.

Theorem not_both_true_and_false : forall P : Prop,
  ~ (P /\ ~P).
Proof.
  unfold not.
  intros P [HP NP].
  apply NP, HP.
Qed.

Theorem de_morgan_not_or : forall (P Q : Prop),
  ~ (P \/ Q) ->
  ~P /\ ~Q.
Proof.
  unfold not.
  intros P Q NPQ.
  split.
  - intros HP. apply NPQ. left. apply HP.
  - intros HQ. apply NPQ. right. apply HQ.
Qed.

Theorem not_true_is_false : forall b : bool,
  b <> true ->
  b = false.
Proof.
  intros b H.
  destruct b eqn:HE.
  - unfold not in H. exfalso. apply H. reflexivity.
  - reflexivity.
Qed.

Lemma True_is_true : True.
Proof. apply I. Qed.

Definition disc_fn (n : nat) : Prop :=
  match n with
  | O => True
  | S _ => False
  end.

Theorem disc_example : forall n,
  ~ (O = S n).
Proof.
  intros n H1.
  assert (H2 : disc_fn O). { simpl. apply I. }
  rewrite H1 in H2.
  simpl in H2.
  apply H2.
Qed.

Module IffPlayground.

Definition iff (P Q : Prop) :=
  (P -> Q) /\ (Q -> P).

Notation "P <-> Q" := (iff P Q)
  (at level 95, no associativity) : type_scope.

End IffPlayground.

Theorem iff_sym : forall P Q : Prop,
  (P <-> Q) ->
  (Q <-> P).
Proof.
  intros P Q [HPQ HQP].
  split.
  - apply HQP.
  - apply HPQ.
Qed.

Lemma not_true_iff_false : forall b,
  b <> true <-> b = false.
Proof.
  intros b.
  split.
  - apply not_true_is_false.
  - intros H.
    rewrite H.
    intros H'.
    discriminate H'.
Qed.

Lemma apply_iff_example1:
  forall P Q R : Prop,
  (P <-> Q) ->
  (Q -> R) ->
  (P -> R).
Proof.
  intros P Q R H1 H2 HP.
  apply H2.
  apply H1.
  apply HP.
Qed.

Lemma apply_iff_example2:
  forall P Q R : Prop,
  (P <-> Q) ->
  (P -> R) ->
  (Q -> R).
Proof.
  intros P Q R H1 H2 HQ.
  apply H2, H1, HQ.
Qed.

Theorem or_distributes_over_and : forall P Q R : Prop,
  P \/ (Q /\ R) <-> (P \/ Q) /\ (P \/ R).
Proof.
  intros P Q R.
  split.
  - intros [HP | [HQ HR]].
    + split.
      * left. apply HP.
      * left. apply HP.
    + split.
      * right. apply HQ.
      * right. apply HR.
  - intros [[HP1 | HQ] [HP2 | HR]].
    + left. apply HP1.
    + left. apply HP1.
    + left. apply HP2.
    + right. split.
      * apply HQ.
      * apply HR.
Qed.

Lemma mul_eq_0 : forall n m,
  n * m = 0 <-> n = 0 \/ m = 0.
Proof.
  split.
  - apply mult_is_O.
  - apply factor_is_O.
Qed.

Theorem or_assoc :
  forall P Q R : Prop,
  P \/ (Q \/ R) <-> (P \/ Q) \/ R.
Proof.
  intros P Q R.
  split.
  - intros [H | [H | H]].
    + left. left. apply H.
    + left. right. apply H.
    + right. apply H.
  - intros [[H | H] | H].
    + left. apply H.
    + right. left. apply H.
    + right. right. apply H.
Qed.

From Coq Require Import Setoids.Setoid.

Lemma mul_eq_0_ternary : forall n m p,
  n * m * p = 0 <->n = 0 \/ m = 0 \/ p = 0.
Proof.
  intros n m p.
  rewrite mul_eq_0.
  rewrite mul_eq_0.
  rewrite or_assoc.
  reflexivity.
Qed.

Definition Even x := exists n : nat, x = double n.

Lemma four_is_Even : Even 4.
Proof.
  unfold Even.
  exists 2.
  reflexivity.
Qed.

Theorem exists_example_2 : forall n,
  (exists m, n = 4 + m) ->
  (exists o, n = 2 + o).
Proof.
  intros n [m H].
  exists (2 + m).
  apply H.
Qed.

Theorem dist_not_exists : forall (X : Type) (P : X -> Prop),
  (forall x, P x) ->
  ~ (exists x, ~ P x).
Proof.
  intros.
  unfold not.
  intros [x Hneg].
  apply Hneg, H.
Qed.

Theorem dist_exists_or : forall (X : Type) (P Q : X -> Prop),
  (exists x, P x \/ Q x) <->
  (exists x, P x) \/ (exists x, Q x).
Proof.
  intros.
  split.
  - intros [x [HP | HQ]].
    + left. exists x. apply HP.
    + right. exists x. apply HQ.
  - intros [[x HP] | [x HQ]].
    + exists x. left. apply HP.
    + exists x. right. apply HQ.
Qed.

Theorem leb_plus_exists : forall n m,
  n <=? m = true ->
  exists x, m = n + x.
Proof.
  intros n.
  induction n.
  - intros m H. exists m. reflexivity.
  - intros m H.
    destruct m.
    + discriminate H.
    + simpl in H. simpl. apply IHn in H.
      destruct H. 
      rewrite H.
      exists x.
      reflexivity.
Qed.

Theorem plus_exists_leb : forall n m,
  (exists x, m = n + x) ->
  n <=? m = true.
Proof.
  intros n m [x H].
  generalize dependent m.
  induction n.
  - reflexivity.
  - intros m H.
    rewrite H.
    simpl.
    apply IHn.
    reflexivity.
Qed.

Fixpoint In {A : Type} (x : A) (l : list A) : Prop :=
  match l with
  | [] => False
  | x' :: l' => x' = x \/ In x l'
  end.

Example In_example_1 : In 4 [1;2;3;4;5].
Proof.
  simpl. right. right. right. left. reflexivity.
Qed.

Example In_example_2:
  forall n, In n [2;4] ->
  exists n', n = 2 * n'.
Proof.
  simpl.
  intros n [H | [H | []]].
  - exists 1. rewrite <- H. reflexivity.
  - exists 2. rewrite <- H. reflexivity.
Qed.

Theorem In_map : forall (A B : Type) (f : A -> B) (l : list A) (x : A),
  In x l ->
  In (f x) (map f l).
Proof.
  intros A B f l x.
  induction l as [| x' l' IHl'].
  - simpl. intros H. apply H.
  - simpl. intros [H | H].
    + rewrite H. left. reflexivity.
    + right. apply IHl', H.
Qed.

Theorem In_map_iff :
  forall (A B : Type) (f : A -> B) (l : list A) (y : B),
  In y (map f l) <->
  exists x, f x = y /\ In x l.
Proof.
  intros A B f l y.
  split.
  - induction l.
    + simpl. intros H. exfalso. apply H.
    + simpl. intros [H | H].
      * exists x. split. apply H. left. reflexivity.
      * apply IHl in H. destruct H as [x0 [H1 H2]].
        exists x0. split. apply H1. right. apply H2.
  - intros [x [H1 H2]].
    rewrite <- H1. apply In_map, H2.
Qed.

Theorem In_app_iff : forall A l l' (a:A),
  In a (l++l') <-> In a l \/ In a l'.
Proof.
  intros A l l' a.
  split.
  - induction l.
    + simpl. intros H. right. apply H.
    + simpl. intros [H | H].
      * left. left. apply H.
      * apply IHl in H. destruct H as [H | H].
        -- left. right. apply H.
        -- right. apply H.
  - induction l.
    + simpl. intros [H | H].
      * exfalso. apply H.
      * apply H.
    + simpl. intros [[H | H] | H].
      * left. apply H.
      * right. apply IHl. left. apply H.
      * right. apply IHl. right. apply H.
Qed.

Fixpoint All {T : Type} (P : T -> Prop) (l : list T) : Prop :=
  match l with
  | [] => True
  | h :: t => (P h) /\ (All P t)
  end.

Theorem All_In : forall T (P : T -> Prop) (l : list T),
  (forall x, In x l -> P x) <-> All P l.
Proof.
  intros T P l.
  split.
  - induction l.
    + simpl. intros H. apply I.
    + simpl. intros H. split.
      * apply H. left. reflexivity.
      * apply IHl. intros y Hy. apply H. right. apply Hy.
  - induction l.
    + simpl. intros Ht x Hf. exfalso. apply Hf.
    + simpl. intros [Hh Ht] y [H | H].
      * rewrite <- H. apply Hh.
      * apply IHl.
        -- apply Ht.
        -- apply H.
Qed.

Definition combine_odd_even (Podd Peven : nat -> Prop) : nat -> Prop :=
  fun (x : nat) => if (odd x) then Podd x else Peven x.

Theorem combine_off_even_intro : forall (Podd Peven : nat -> Prop) (n : nat),
  (odd n = true -> Podd n) ->
  (odd n = false -> Peven n) ->
  combine_odd_even Podd Peven n.
Proof.
  intros Podd Peven n H1 H2.
  unfold combine_odd_even.
  destruct (odd n) eqn:E.
  - apply H1. reflexivity.
  - apply H2. reflexivity.
Qed.

Theorem combine_odd_even_elim_odd :
  forall (Podd Peven : nat -> Prop) (n : nat),
  combine_odd_even Podd Peven n ->
  odd n = true ->
  Podd n.
Proof.
  intros Podd Peven n H1 H2.
  unfold combine_odd_even in H1.
  rewrite H2 in H1.
  apply H1.
Qed.

Theorem combine_odd_even_elim_even :
  forall (Podd Peven : nat -> Prop) (n : nat),
  combine_odd_even Podd Peven n ->
  odd n = false ->
  Peven n.
Proof.
  intros Podd Peven n H1 H2.
  unfold combine_odd_even in H1.
  rewrite H2 in H1.
  apply H1.
Qed.

(* Applying theorems to arguments *)