From 53ebca85280c62dfcae12ff1fd0ed3e7a931d111 Mon Sep 17 00:00:00 2001 From: Peter Mikkelsen Date: Mon, 8 May 2023 21:55:42 +0200 Subject: [PATCH] Finish logic chapter --- vol1/Logic.v | 517 ++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 516 insertions(+), 1 deletion(-) diff --git a/vol1/Logic.v b/vol1/Logic.v index 2ce8166..24e4d5c 100644 --- a/vol1/Logic.v +++ b/vol1/Logic.v @@ -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 -- 2.43.4