~pmikkelsen/software-foundations

b9decb3a75bf85899ffeb37896ca4eb2284a49aa — Peter Mikkelsen 1 year, 1 month ago 53ebca8 master
Disable some warnings, and start IndProp chapter
4 files changed, 203 insertions(+), 0 deletions(-)

M vol1/IndProp.v
M vol1/Logic.v
M vol1/Poly.v
M vol1/Tactics.v
M vol1/IndProp.v => vol1/IndProp.v +200 -0
@@ 0,0 1,200 @@
Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality".
From LF Require Export Logic.
From Coq Require Import Lia.

Fixpoint div2 (n : nat) :=
  match n with
  | 0 => 0
  | 1 => 0
  | S (S n) => S (div2 n)
  end.

Definition f (n : nat) :=
  if even n
  then div2 n
  else (3 * n) + 1.

Fail Fixpoint reaches_1_in (n : nat) :=
  if n =? 1 then 0
  else 1 + reaches_1_in (f n).

Inductive reaches_1 : nat -> Prop :=
  | term_done : reaches_1 1
  | term_more (n : nat) : reaches_1 (f n) -> reaches_1 n.

Conjecture collatz : forall n, reaches_1 n.

Module LePlayground.

Inductive le : nat -> nat -> Prop :=
  | le_n (n : nat) : le n n
  | le_S (n m : nat) : le n m -> le n (S m).

End LePlayground.

Inductive clos_trans {X : Type} (R : X -> X -> Prop) : X -> X -> Prop :=
  | t_step (x y : X) : R x y -> clos_trans R x y
  | t_trans (x y z : X) :
    clos_trans R x y ->
    clos_trans R y z ->
    clos_trans R x z.

Inductive Perm3 {X : Type} : list X -> list X -> Prop :=
  | perm3_swap12 (a b c : X) : Perm3 [a;b;c] [b;a;c]
  | perm3_swap23 (a b c : X) : Perm3 [a;b;c] [a;c;b]
  | perm3_trans (l1 l2 l3 : list X) :
    Perm3 l1 l2 -> Perm3 l2 l3 -> Perm3 l1 l3.

Example perm_test1 : Perm3 [3;2;1] [1;2;3].
Proof.
  apply perm3_trans with [2;3;1].
  - apply perm3_swap12.
  - apply perm3_trans with [2;1;3].
    + apply perm3_swap23.
    + apply perm3_swap12.
Qed.

Example perm_test2 : Perm3 [1;2;3] [1;2;3].
Proof.
  apply perm3_trans with [1;3;2].
  - apply perm3_swap23.
  - apply perm3_swap23.
Qed.

Inductive ev : nat -> Prop :=
  | ev_0 : ev 0
  | ev_SS (n : nat) (H : ev n) : ev (S (S n)).

Theorem ev_4 : ev 4.
Proof. apply ev_SS. apply ev_SS. apply ev_0. Qed.

Theorem ev_4' : ev 4.
Proof. apply (ev_SS 2 (ev_SS 0 ev_0)). Qed.

Theorem ev_plus4 : forall n, ev n -> ev (4 + n).
Proof.
  intros n.
  simpl.
  intros Hn.
  apply ev_SS.
  apply ev_SS.
  apply Hn.
Qed.

Theorem ev_double : forall n,
  ev (double n).
Proof.
  intros n.
  induction n.
  - simpl. apply ev_0.
  - simpl. apply ev_SS. apply IHn.
Qed.

Theorem ev_inversion : forall (n : nat),
  ev n ->
  (n = 0) \/ (exists n', n = S (S n') /\ ev n').
Proof.
  intros n E.
  destruct E as [| n' E'] eqn:EE.
  - left. reflexivity.
  - right. exists n'. split. reflexivity. apply E'.
Qed.

Theorem evSS_ev : forall n, ev (S (S n)) -> ev n.
Proof.
  intros n H.
  apply ev_inversion in H.
  destruct H as [H0 | H1].
  - discriminate H0.
  - destruct H1 as [n' [Hnm Hev]].
    injection Hnm as Heq.
    rewrite Heq. apply Hev.
Qed.

Theorem evSS_ev' : forall n,
  ev (S (S n)) -> ev n.
Proof.
  intros n E.
  inversion E as [| n' E' Heq].
  apply E'.
Qed.

Theorem one_not_even : ~ ev 1.
Proof.
  intros H. apply ev_inversion in H. destruct H as [ | [m [Hm _]]].
  - discriminate H.
  - discriminate Hm.
Qed.

Theorem one_not_even' : ~ ev 1.
Proof.
  intros H. inversion H.
Qed.

Theorem SSSSev__even : forall n,
  ev (S (S (S (S n)))) -> ev n.
Proof.
  intros n H.
  inversion H as [| n' E' Heq].
  inversion E' as [ |n'' E'' Heq'].
  apply E''.
Qed.

Theorem ev5_nonsense :
  ev 5 -> 2 + 2 = 9.
Proof.
  intros H.
  inversion H as [| n' H' Heq'].
  inversion H' as [| n'' H'' Heq''].
  inversion H''.
Qed.

Theorem inversion_ex1 : forall (n m o : nat),
  [n; m] = [o; o] -> [n] = [m].
Proof.
  intros n m o H.
  inversion H.
  reflexivity.
Qed.

Theorem inversion_ex2 : forall (n : nat),
  S n = O -> 2 + 2 = 5.
Proof.
  intros n H.
  inversion H.
Qed.

Theorem ev_Even_firsttry : forall n,
  ev n -> Even n.
Proof.
  unfold Even.
  intros n E. inversion E as [EQ' | n' E' EQ'].
  - exists 0. reflexivity.
  - assert (H: (exists k', n' = double k')
               -> (exists n0, S (S n') = double n0)).
    { intros [k' EQ'']. exists (S k'). simpl. rewrite <- EQ''. reflexivity. }
  apply H.
  generalize dependent E'.
Abort.

Lemma ev_Even: forall n,
  ev n -> Even n.
Proof.
  intros n E.
  induction E as [| n' E' IH].
  - unfold Even. exists 0. reflexivity.
  - unfold Even in IH.
    destruct IH as [k Hk].
    rewrite Hk.
    unfold Even.
    exists (S k). reflexivity.
Qed.

Theorem ev_Even_iff : forall n,
  ev n <-> Even n.
Proof.
  intros n. split.
  - apply ev_Even.
  - unfold Even. intros [k Hk]. rewrite Hk. apply ev_double.
Qed.


M vol1/Logic.v => vol1/Logic.v +1 -0
@@ 1,3 1,4 @@
Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality".
From LF Require Export Tactics.

Theorem plus_2_2_is_4:

M vol1/Poly.v => vol1/Poly.v +1 -0
@@ 1,3 1,4 @@
Set Warnings "-notation-overridden,-parsing".
From LF Require Export Lists.

Inductive boollist : Type :=

M vol1/Tactics.v => vol1/Tactics.v +1 -0
@@ 1,3 1,4 @@
Set Warnings "-notation-overridden,-parsing".
From LF Require Export Poly.

Theorem silly1 : forall (n m : nat),