(* week-11_induction-principles-colon-strong-induction.v *) (* Time-stamp: <2025-07-08 17:13:17 olivier> *) (* LPP 2025 - CS3234 2024-2025, Sem2 *) (* Olivier Danvy *) (* Version of 02 Jul 2025 *) (* ********** *) Ltac fold_unfold_tactic name := intros; unfold name; fold name; reflexivity. Require Import Arith Bool. (* ********** *) (* First-, second-, and third-order mathematical induction: *) (* ***** *) Lemma nat_ind1 : forall P : nat -> Prop, P 0 -> (forall n' : nat, P n' -> P (S n')) -> forall n : nat, P n. Proof. Admitted. (* ***** *) Lemma nat_ind2 : forall P : nat -> Prop, P 0 -> P 1 -> (forall n' : nat, P n' -> P (S n') -> P (S (S n'))) -> forall n : nat, P n. Proof. Admitted. (* ***** *) Lemma nat_ind3 : forall P : nat -> Prop, P 0 -> P 1 -> P 2 -> (forall n' : nat, P n' -> P (S n') -> P (S (S n')) -> P (S (S (S n')))) -> forall n : nat, P n. Proof. Admitted. (* ********** *) (* Course-of-values induction: *) Fixpoint conjunction_upto (n : nat) (P : nat -> Prop) : Prop := match n with | 0 => P 0 | S n' => P (S n') /\ conjunction_upto n' P end. Lemma fold_unfold_conjunction_upto_O : forall P : nat -> Prop, conjunction_upto 0 P = P 0. Proof. fold_unfold_tactic conjunction_upto. Qed. Lemma fold_unfold_conjunction_upto_S : forall (n' : nat) (P : nat -> Prop), conjunction_upto (S n') P = (P (S n') /\ conjunction_upto n' P). Proof. fold_unfold_tactic conjunction_upto. Qed. (* ***** *) Lemma conjunction_upto_a_number_implies_the_property_at_this_number : forall (n : nat) (P : nat -> Prop), conjunction_upto n P -> P n. Proof. Admitted. Lemma conjunction_upto_a_number_implies_the_property_at_O : forall (n : nat) (P : nat -> Prop), conjunction_upto n P -> P 0. Proof. Admitted. Lemma conjunction_upto_an_addition_implies_conjunction_upto_the_addend : forall (k1 k2 : nat) (P : nat -> Prop), conjunction_upto (k1 + k2) P -> conjunction_upto k2 P. Proof. Admitted. (* ***** *) Lemma nat_ind_course_of_values : forall P : nat -> Prop, P 0 -> (forall n' : nat, conjunction_upto n' P -> P (S n')) -> forall n : nat, P n. Proof. Admitted. (* ********** *) Lemma conjunction_upto_implies_any_one_of_them : forall (y : nat) (P : nat -> Prop), conjunction_upto y P -> forall x : nat, x <= y -> P x. Proof. Admitted. Lemma any_one_of_them_implies_conjunction_upto : forall (y : nat) (P : nat -> Prop), (forall x : nat, x <= y -> P x) -> conjunction_upto y P. Proof. Admitted. Theorem the_same_dame : forall P : nat -> Prop, (forall m : nat, (forall i : nat, i <= m -> P i) -> P (S m)) <-> (forall m : nat, conjunction_upto m P -> P (S m)). Proof. Admitted. Lemma nat_ind_strong : forall P : nat -> Prop, P 0 -> (forall n' : nat, (forall i : nat, i <= n' -> P i) -> P (S n')) -> forall n : nat, P n. Proof. intros P P_O P_S. destruct (the_same_dame P) as [strong_implies_course_of_values _]. exact (nat_ind_course_of_values P P_O (strong_implies_course_of_values P_S)). Qed. (* ********** *) (* Exercise 25 *) Lemma nat_ind_course_of_values_using_nat_strong : forall P : nat -> Prop, P 0 -> (forall n' : nat, conjunction_upto n' P -> P (S n')) -> forall n : nat, P n. Proof. Abort. (* ********** *) (* Exercise 26 *) Lemma nat_ind1_using_strong_induction : forall P : nat -> Prop, P 0 -> (forall n' : nat, P n' -> P (S n')) -> forall n : nat, P n. Proof. Abort. (* ********** *) (* Exercise 27 *) (* ***** *) (* Exercise 27a *) Lemma nat_ind2_using_strong_induction : forall P : nat -> Prop, P 0 -> P 1 -> (forall n' : nat, P n' -> P (S n') -> P (S (S n'))) -> forall n : nat, P n. Proof. intros P P_0 P_1 P_SS n. induction n as [ | [ | n'] IHn'] using nat_ind_strong. - exact P_0. - exact P_1. - Check (IHn' (S n') (Nat.le_refl (S n'))). Search (_ <= S _). Check (Nat.le_succ_diag_r n'). Check (IHn' n' (Nat.le_succ_diag_r n')). exact (P_SS n' (IHn' n' (Nat.le_succ_diag_r n')) (IHn' (S n') (Nat.le_refl (S n')))). Qed. (* ***** *) (* Exercise 27b *) Lemma nat_ind2_0_using_strong_induction : forall P : nat -> Prop, P 0 -> P 1 -> (forall n' : nat, P n' -> P (S (S n'))) -> forall n : nat, P n. Proof. intros P P_0 P_1 P_SS n. induction n as [ | [ | n'] IHn'] using nat_ind_strong. - exact P_0. - exact P_1. - Search (_ <= S _). Check (Nat.le_succ_diag_r n'). Check (IHn' n' (Nat.le_succ_diag_r n')). exact (P_SS n' (IHn' n' (Nat.le_succ_diag_r n'))). Qed. (* ***** *) (* Exercise 27c *) Lemma nat_ind2_1_using_strong_induction : forall P : nat -> Prop, P 0 -> P 1 -> (forall n' : nat, P (S n') -> P (S (S n'))) -> forall n : nat, P n. Proof. intros P P_0 P_1 P_SS n. induction n as [ | [ | n'] IHn'] using nat_ind_strong. - exact P_0. - exact P_1. - exact (P_SS n' (IHn' (S n') (Nat.le_refl (S n')))). Qed. (* ********** *) (* Exercise 28 *) Lemma nat_ind3_using_strong_induction : forall P : nat -> Prop, P 0 -> P 1 -> P 2 -> (forall n' : nat, P n' -> P (S n') -> P (S (S n')) -> P (S (S (S n')))) -> forall n : nat, P n. Proof. Abort. (* ********** *) (* Exercise 29 *) Lemma nat_ind4_using_strong_induction : forall P : nat -> Prop, P 0 -> P 1 -> P 2 -> P 3 -> (forall n' : nat, P n' -> P (S n') -> P (S (S n')) -> P (S (S (S n'))) -> P (S (S (S (S n'))))) -> forall n : nat, P n. Proof. Abort. (* ********** *) (* Exercise 30 *) Fixpoint evenp2 (n : nat) : bool := match n with O => true | S n' => match n' with O => false | S n'' => evenp2 n'' end end. Lemma fold_unfold_evenp2_O : evenp2 O = true. Proof. fold_unfold_tactic evenp2. Qed. Lemma fold_unfold_evenp2_S : forall n' : nat, evenp2 (S n') = match n' with O => false | S n'' => evenp2 n'' end. Proof. fold_unfold_tactic evenp2. Qed. Corollary fold_unfold_evenp2_1 : evenp2 (S O) = false. Proof. rewrite -> fold_unfold_evenp2_S. reflexivity. Qed. Corollary fold_unfold_evenp2_SS : forall n'' : nat, evenp2 (S (S n'')) = evenp2 n''. Proof. intro n''. rewrite -> fold_unfold_evenp2_S. reflexivity. Qed. Lemma two_times_S : forall n : nat, S (S (2 * n)) = 2 * S n. Proof. intro n. ring. Qed. Lemma first_base_case_for_soundness_and_completeness_of_evenp2 : evenp2 0 = true <-> (exists m : nat, 0 = 2 * m). Proof. Admitted. Lemma second_base_case_for_soundness_and_completeness_of_evenp2 : evenp2 1 = true <-> (exists m : nat, 1 = 2 * m). Proof. rewrite -> fold_unfold_evenp2_1. split. + intros H_absurd. discriminate H_absurd. + intros [[ | m'] H_m']. * rewrite -> Nat.mul_0_r in H_m'. discriminate H_m'. * rewrite <- two_times_S in H_m'. discriminate H_m'. Admitted. Lemma common_part_of_induction_step_for_soundness_and_completeness_of_evenp2 : forall (n' : nat) (IHn'_sound : evenp2 n' = true -> exists m : nat, n' = 2 * m) (IHn'_complete : (exists m : nat, n' = 2 * m) -> evenp2 n' = true), evenp2 n' = true <-> (exists m : nat, S (S n') = 2 * m). Proof. Admitted. Theorem soundness_and_completeness_of_evenp2_using_strong_induction : forall n : nat, evenp2 n = true <-> exists m : nat, n = 2 * m. Proof. intro n. induction n as [ | [ | n'] IHn'] using nat_ind_strong. - exact first_base_case_for_soundness_and_completeness_of_evenp2. - exact second_base_case_for_soundness_and_completeness_of_evenp2. - admit. Abort. (* ********** *) (* Exercise 31 *) Fixpoint ternaryp (n : nat) : bool := match n with 0 => true | 1 => false | 2 => false | S (S (S n')) => ternaryp n' end. Lemma fold_unfold_ternaryp_O : ternaryp 0 = true. Proof. fold_unfold_tactic ternaryp. Qed. Lemma fold_unfold_ternaryp_1 : ternaryp 1 = false. Proof. fold_unfold_tactic ternaryp. Qed. Lemma fold_unfold_ternaryp_2 : ternaryp 2 = false. Proof. fold_unfold_tactic ternaryp. Qed. Lemma fold_unfold_ternaryp_SSS : forall n' : nat, ternaryp (S (S (S n'))) = ternaryp n'. Proof. fold_unfold_tactic ternaryp. Qed. Theorem soundness_and_completeness_of_ternaryp_using_strong_induction : forall n : nat, ternaryp n = true <-> exists m : nat, n = 3 * m. Proof. Abort. (* ********** *) (* Exercise 32 *) Property threes_and_fives_using_strong_induction : forall n : nat, exists a b : nat, 8 + n = 3 * a + 5 * b. Proof. Abort. (* ********** *) (* Exercise 33 *) Property fours_and_fives_using_strong_induction : forall n : nat, exists a b : nat, 12 + n = 4 * a + 5 * b. Proof. Abort. (* ********** *) (* end of week-11_induction-principles-colon-strong-induction.v *)