~pmikkelsen/software-foundations

53ebca85280c62dfcae12ff1fd0ed3e7a931d111 — Peter Mikkelsen 1 year, 1 month ago 37fce3f
Finish logic chapter
1 files changed, 516 insertions(+), 1 deletions(-)

M vol1/Logic.v
M vol1/Logic.v => vol1/Logic.v +516 -1
@@ 619,5 619,520 @@ Proof.
  apply H1.
Qed.

(* Applying theorems to arguments *)
Lemma add_comm3 :
  forall x y z,
  x + (y + z) = (z + y) + x.
Proof.
  intros x y z.
  rewrite add_comm.
  rewrite add_comm.
Abort.

Lemma add_comm3_take2 :
  forall x y z,
  x + (y + z) = (z + y) + x.
Proof.
  intros x y z.
  rewrite add_comm.
  assert (H: y + z = z + y).
    { rewrite add_comm. reflexivity. }
  rewrite H.
  reflexivity.
Qed.

Lemma add_comm3 :
  forall x y z,
  x + (y + z) = (z + y) + x.
Proof.
  intros x y z.
  rewrite add_comm.
  rewrite (add_comm y z).
  reflexivity.
Qed.

Theorem in_not_nil : forall A (x : A) (l : list A),
  In x l ->
  l <> [].
Proof.
  intros A x l H.
  unfold not.
  intros Hl.
  rewrite Hl in H.
  simpl in H.
  apply H.
Qed.

Lemma in_not_nil_42 : 
  forall l : list nat,
  In 42 l ->
  l <> [].
Proof.
  intros l H.
  Fail apply in_not_nil.
Abort.

Lemma in_not_nil_42_take2 : 
  forall l : list nat,
  In 42 l ->
  l <> [].
Proof.
  intros l H.
  apply in_not_nil with (x := 42).
  apply H.
Qed.

Lemma in_not_nil_42_take3 : 
  forall l : list nat,
  In 42 l ->
  l <> [].
Proof.
  intros l H.
  apply in_not_nil in H.
  apply H.
Qed.

Lemma in_not_nil_42_take4 :
  forall l : list nat,
  In 42 l ->
  l <> [].
Proof.
  intros l H.
  apply (in_not_nil nat 42).
  apply H.
Qed.

Lemma in_not_nil_42_take5 :
  forall l : list nat,
  In 42 l ->
  l <> [].
Proof.
  intros l H.
  apply (in_not_nil _ _ _ H).
Qed.

Example lemma_application_ex :
  forall {n : nat} {ns : list nat},
  In n (map (fun m => m * 0) ns) ->
  n = 0.
Proof.
  intros n ns H.
  destruct (proj1 _ _ (In_map_iff _ _ _ _ _) H) as [m [Hm _]].
  rewrite mul_0_r in Hm.
  rewrite <- Hm.
  reflexivity.
Qed.

Example function_equality_ex1 :
  (fun x => 3 + x) = (fun x => (pred 4) + x).
Proof. reflexivity. Qed.

Example function_equality_ex2 :
  (fun x => plus x 1) = (fun x => plus 1 x).
Proof.
Abort.

Axiom functional_extensionality : forall {X Y : Type} {f g : X -> Y},
  (forall (x : X), f x = g x) -> f = g.

Example function_equality_ex2 :
  (fun x => plus x 1) = (fun x => plus 1 x).
Proof.
  apply functional_extensionality.
  intros x.
  apply add_comm.
Qed.

Fixpoint rev_append {X} (l1 l2 : list X) : list X :=
  match l1 with
  | [] => l2
  | x :: l1' => rev_append l1' (x :: l2)
  end.

Definition tr_rev {X} (l : list X) : list X :=
  rev_append l [].

Theorem rev_append_x : forall X (x y : list X),
  rev_append x y = rev x ++ y.
Proof.
  intros X x.
  induction x.
  - reflexivity.
  - simpl. intros y.
    rewrite IHx.
    rewrite <- app_assoc.
    reflexivity.
Qed.

Theorem tr_rev_correct : forall X,
  @tr_rev X = @rev X.
Proof.
  intros X.
  apply functional_extensionality.
  intros x.
  induction x.
  - reflexivity.
  - unfold tr_rev.
    simpl. apply rev_append_x.
Qed.

Example even_42_bool : even 42 = true.
Proof. reflexivity. Qed.

Example even_42_prop : Even 42.
Proof. unfold Even. exists 21. reflexivity. Qed.

Lemma even_double : forall k, even (double k) = true.
Proof.
  induction k.
  - reflexivity.
  - simpl. apply IHk.
Qed.

Lemma negb_flip : forall e b,
  negb e = b ->
  e = negb b.
Proof.
  intros.
  destruct e.
  - destruct b.
    + discriminate H.
    + reflexivity.
  - destruct b.
    + reflexivity.
    + discriminate H.
Qed.

Lemma even_double_conv : forall n, exists k,
  n = if even n then double k else S (double k).
Proof.
  intros n.
  induction n.
  - simpl. exists 0. reflexivity.
  - destruct IHn as [k IHn].
    destruct (even (S n)) eqn:E.
    + rewrite even_S in E.
      rewrite (negb_flip _ _ E) in IHn.
      simpl in IHn.
      exists (S k).
      simpl. rewrite IHn. reflexivity.
    + rewrite even_S in E.
      rewrite (negb_flip _ _ E) in IHn.
      simpl in IHn.
      exists k.
      rewrite IHn.
      reflexivity.
Qed.

Theorem even_bool_prop : forall n,
  even n = true <-> Even n.
Proof.
  intros n.
  split.
  - intros H.
    destruct (even_double_conv n) as [k Hk].
    rewrite Hk. rewrite H. exists k. reflexivity.
  - intros [k Hk].
    rewrite Hk. apply even_double.
Qed.

Theorem eqb_eq : forall n1 n2 : nat,
  n1 =? n2 = true <-> n1 = n2.
Proof.
  intros n1 n2.
  split.
  - apply eqb_true.
  - intros H.
    rewrite H.
    apply eqb_refl.
Qed.

Fail
Definition is_even_prime n :=
  if n = 2 then true
  else false.

Example even_1000 : Even 1000.
Proof. unfold even. exists 500. reflexivity. Qed.

Example even_1000' : even 1000 = true.
Proof. reflexivity. Qed.

Example even_1000'' : Even 1000.
Proof. apply even_bool_prop. reflexivity. Qed.

Example not_even_1001 : even 1001 = false.
Proof. reflexivity. Qed.

Example not_even_1001' : ~(Even 1001).
Proof.
  rewrite <- even_bool_prop.
  unfold not.
  simpl.
  intro H.
  discriminate H.
Qed.

Lemma plus_eqb_example : forall n m p : nat,
  n =? m = true ->
  n + p =? m + p = true.
Proof.
  intros n m p H.
  rewrite eqb_eq in H.
  rewrite H.
  rewrite eqb_eq.
  reflexivity.
Qed.

Theorem andb_true_iff : forall b1 b2 : bool,
  b1 && b2 = true <-> b1 = true /\ b2 = true.
Proof.
  intros b1 b2.
  split.
  - destruct b1 eqn:Eb1.
    + intros H. split.
      * reflexivity.
      * rewrite <- H. reflexivity.
    + simpl. intros H. discriminate H.
  - intros [H1 H2].
    rewrite H1, H2.
    reflexivity.
Qed.

Theorem orb_true_iff : forall b1 b2,
  b1 || b2 = true <-> b1 = true \/ b2 = true.
Proof.
  intros b1 b2.
  split.
  - destruct b1 eqn:Eb1.
    + simpl. intros H. left. apply H.
    + simpl. intros H. right. apply H.
  - intros [H | H].
    + rewrite H. reflexivity.
    + rewrite H. destruct b1.
      * reflexivity.
      * reflexivity.
Qed.

Theorem eqb_neq : forall x y,
  x =? y = false <->
  x <> y.
Proof.
  intros x y.
  split.
  - unfold not.
    intros H1 H2.
    rewrite <- eqb_eq in H2.
    rewrite H1 in H2.
    discriminate H2.
  - rewrite <- eqb_eq.
    apply not_true_iff_false.
Qed.

Fixpoint eqb_list {A : Type} (eqb : A -> A -> bool) (l1 l2 : list A) : bool :=
  match l1, l2 with
  | [], [] => true
  | (a :: aa), (b :: bb) => andb (eqb a b) (eqb_list eqb aa bb)
  | _, _ => false
  end.

Theorem eqb_list_true_iff :
  forall A (eqb : A -> A -> bool),
    (forall a1 a2, eqb a1 a2 = true <-> a1 = a2) ->
    forall l1 l2, eqb_list eqb l1 l2 = true <-> l1 = l2.
Proof.
  intros A eqb H l1 l2.
  split.
  - generalize dependent l2.
    induction l1.
    + induction l2.
      * reflexivity.
      * simpl. intros contra. discriminate contra.
    + induction l2.
      * simpl. intros contra. discriminate contra.
      * simpl. rewrite andb_true_iff. intros [H1 H2].
        rewrite H in H1.
        rewrite H1.
        rewrite (IHl1 l2 H2).
        reflexivity.
  - generalize dependent l2.
    induction l1.
    + induction l2.
      * reflexivity.
      * simpl. intros contra. discriminate contra.
    + induction l2.
      * simpl. intros contra. discriminate contra.
      * intros Heq. rewrite <- Heq. simpl.
        rewrite andb_true_iff.
        split.
        -- rewrite H. reflexivity.
        -- rewrite IHl1. reflexivity. reflexivity.
Qed.

Fixpoint forallb {X : Type} (test : X -> bool) (l : list X) : bool :=
  match l with
  | [] => true
  | h :: t => andb (test h) (forallb test t)
  end.

Theorem forallb_true_iff : forall X test (l : list X),
  forallb test l = true <-> All (fun x => test x = true) l.
Proof.
  intros X test l.
  split.
  - induction l.
    + simpl. reflexivity.
    + simpl. rewrite andb_true_iff. intros [H1 H2]. split.
      * apply H1.
      * apply IHl, H2.
  - induction l.
    + reflexivity.
    + simpl. intros [H1 H2].
      rewrite andb_true_iff. split.
      * apply H1.
      * apply IHl, H2.
Qed.

Definition excluded_middle := forall P : Prop,
  P \/ ~P.

Theorem restricted_excluded_middle : forall P b,
  (P <-> b = true) ->
  P \/ ~P.
Proof.
  intros P [] H.
  - left. rewrite H. reflexivity.
  - right. rewrite H. intros contra. discriminate contra.
Qed.

Theorem restricted_excluded_middle_eq : forall (n m : nat),
  n = m \/ n <> m.
Proof.
  intros n m.
  apply (restricted_excluded_middle (n = m) (n =? m)).
  symmetry.
  apply eqb_eq.
Qed.

Theorem excluded_middle_irrefutable : forall (P : Prop),
  ~ ~ (P \/ ~P).
Proof.
  intros P H.
  apply de_morgan_not_or in H.
  destruct H as [H1 H2].
  apply H2 in H1.
  apply H1.
Qed.

Theorem not_exists_dist :
  excluded_middle ->
  forall (X:Type) (P : X -> Prop),
    ~ (exists x, ~ P x) -> (forall x, P x).
Proof.
  unfold excluded_middle.
  unfold not.
  intros EX X P H x.
  destruct (EX (P x)) as [Htrue | Hfalse].
  - apply Htrue.
  - exfalso. apply H. exists x. apply Hfalse.
Qed.

Definition peirce := forall P Q : Prop,
  ((P -> Q) -> P) -> P.

Definition double_negation_elimination := forall P : Prop,
  ~~P -> P.

Definition de_morgan_not_and_not := forall P Q : Prop,
  ~(~P /\ ~Q) -> P \/ Q.

Definition implies_to_or := forall P Q : Prop,
  (P -> Q) -> (~P \/ Q).

Theorem excluded_middle_eq_peirce : excluded_middle <-> peirce.
Proof.
  unfold peirce, excluded_middle, not.
  split.
  - intros H P Q Hpq.
    destruct (H P) as [Hp | Hnotp].
    + apply Hp.
    + apply Hpq. intros Hp. exfalso. apply Hnotp, Hp.
  - intros.
    apply H with (Q := False).
    intros Hf.
    right.
    intros Hp.
    apply Hf.
    left.
    apply Hp.
Qed.

Theorem peirce_eq_double_negation_elimination : peirce <-> double_negation_elimination.
Proof.
  unfold peirce, double_negation_elimination, not.
  split.
  - intros H1 P H2.
    apply H1 with (Q := False).
    intros H3.
    exfalso.
    apply H2, H3.
  - intros H1 P Q H2.
    apply H1.
    intros H3.
    apply H3,H2.
    intros Hp.
    exfalso.
    apply H3,Hp.
Qed.

Theorem double_negation_elimination_eq_de_morgan_not_and_not : double_negation_elimination <-> de_morgan_not_and_not.
Proof.
  unfold double_negation_elimination, de_morgan_not_and_not, not.
  split.
  - intros H1 P Q H2.
    apply H1.
    intros H3.
    apply H2.
    split.
    + intros Hp. apply H3. left. apply Hp.
    + intros Hq. apply H3. right. apply Hq.
  - intros H1 P H2.
    destruct (H1 P P).
    + intros [Hp _].
      apply H2, Hp.
    + apply H.
    + apply H.
Qed.

Theorem de_morgan_not_and_not_eq_implies_to_or : de_morgan_not_and_not <-> implies_to_or.
Proof.
  unfold de_morgan_not_and_not, implies_to_or, not.
  split.
  - intros H1 P Q PQ.
    apply H1.
    intros [H2 H3].
    apply H2.
    intros Hp.
    apply H3.
    apply PQ.
    apply Hp.
  - intros H1 P Q H2.
    destruct (H1 P P).
    + intros Hp. apply Hp.
    + destruct (H1 Q Q).
      * intros Hq. apply Hq.
      * exfalso. apply H2.
        split. apply H. apply H0.
      * right. apply H0.
    + left. apply H.
Qed.

Theorem implies_to_or_eq_excluded_middle : implies_to_or <-> excluded_middle.
Proof.
  transitivity de_morgan_not_and_not.
  symmetry. apply de_morgan_not_and_not_eq_implies_to_or.
  transitivity double_negation_elimination.
  symmetry. apply double_negation_elimination_eq_de_morgan_not_and_not.
  transitivity peirce.
  symmetry. apply peirce_eq_double_negation_elimination.
  symmetry. apply excluded_middle_eq_peirce.
Qed. (* We now went full circle *)
\ No newline at end of file