From 45a55a2b6ac24cd0499b875efebd11625c4a10b8 Mon Sep 17 00:00:00 2001 From: smolka Date: Mon, 14 Aug 2023 12:13:09 +0200 Subject: [PATCH] 2023 --- coq/cty.v | 13 ++++ coq/list.v | 201 +++++++++++++++++++++++++++++++++++++++++------------ coq/nat.v | 75 +++++++++++++++----- 3 files changed, 229 insertions(+), 60 deletions(-) diff --git a/coq/cty.v b/coq/cty.v index 1fe5fe1..3cb7dc7 100644 --- a/coq/cty.v +++ b/coq/cty.v @@ -666,6 +666,19 @@ Definition serial_list A := forall n, S n el A -> n el A. Fact serial_list_nrep A : serial_list A -> nrep A -> forall k, k el A <-> k < length A. +Proof. + intros H1 H2. + induction A as [|x A IH]; cbn. + - intuition lia. + - intros k. split. + + intros [->|H4]. + * admit. + * enough (k < length A) by lia. + apply IH. + -- admit. + -- apply H2. + + Admitted. Definition fin_alignment_cutoff X f n : diff --git a/coq/list.v b/coq/list.v index a5bd5eb..3a3ff5c 100644 --- a/coq/list.v +++ b/coq/list.v @@ -2,13 +2,19 @@ From Coq Require Import Arith Lia. Unset Elimination Schemes. Definition dec (X: Type) : Type := X + (X -> False). Definition eqdec X := forall x y: X, dec (x = y). -Definition nat_eqdec : eqdec nat := - fun x y => match Nat.eq_dec x y with left H => inl H | right H => inr H end. +Definition decider {X} (p: X -> Type) := forall x, dec (p x). +Definition nat_eqdec : eqdec nat. +Proof. + hnf; induction x as [|x IH]; destruct y as [|y]; unfold dec in *. + 1-3: intuition congruence. + destruct (IH y); intuition congruence. +Qed. +Notation sig := sigT. Notation "'Sigma' x .. y , p" := - (sigT (fun x => .. (sigT (fun y => p%type)) ..)) + (sigT (fun x => .. (sig (fun y => p%type)) ..)) (at level 200, x binder, right associativity, format "'[' 'Sigma' '/ ' x .. y , '/ ' p ']'") - : type_scope. + : type_scope. Definition XM := forall P, P \/ ~P. @@ -160,6 +166,18 @@ Section List. * right. cbn. intuition. Defined. + Definition list_dec (p: X -> Prop) A : + decider p -> (Sigma x, x el A /\ p x) + (forall x, x el A -> ~p x). + Proof. + intros d. + induction A as [|y A [(x&IH1&IH2)|IH]]; cbn. + - intuition. + - left. exists x. auto. + - destruct (d y) as [H|H]. + + left. exists y. auto. + + right. intros x [->|H1]; auto. + Qed. + (*** Inclusion and Equivalence *) Definition equi A B := A <<= B /\ B <<= A. @@ -234,7 +252,7 @@ Section List. * cbn. congruence. Qed. - (*** Non-Repeating Lists *) + (*** Nonrepeating Lists *) Fixpoint rep A : Prop := match A with @@ -391,7 +409,7 @@ Section List. apply IH. exact H2. firstorder congruence. Qed. - (*** Constructive Discrimination *) + (*** Constructive Discrimination *) Fact nrep_discriminate_ex {A B} : XM -> nrep A -> length B < length A -> exists x, x el A /\ x nel B. @@ -664,7 +682,6 @@ Section List. * right. apply rem_el. auto. Qed. - (*** Sub and Pos *) Section SubPos. @@ -748,6 +765,9 @@ Section List. * apply IH. intros (z&H1&H2). eauto. Qed. End List. + +Arguments equi {X}. +Arguments list_dec {X}. Arguments mem_dec {X}. Arguments mem_sum {X}. Arguments nrep {X}. @@ -790,59 +810,94 @@ Qed. (*** Lists of Numbers *) -Fixpoint seq n k : list nat := - match k with - 0 => [] - | S k' => n :: seq (S n) k' - end. +Definition segment A := forall k, k el A <-> k < length A. +Definition serial (A: list nat) := forall n k, n el A -> k <= n -> k el A. -Fact seq_length n k : - length (seq n k) = k. +Fact segment_nil : + segment []. Proof. - induction k as [|k IH] in n |-*; cbn. - - reflexivity. - - f_equal. apply IH. + intros k. cbn; intuition; lia. Qed. -Fact seq_in x n k : - x el seq n k <-> n <= x < n + k. +Fact segment_equal A B : + segment A -> segment B -> length A = length B -> A <<= B. Proof. - induction k as [|k IH] in n |-*; cbn. - - lia. - - rewrite IH. lia. + intros H1 H2 E x H3%H1. apply H2. lia. Qed. -Fact seq_nrep n k : - nrep (seq n k). +Fact segment_serial A : + segment A -> serial A. Proof. - induction k as [|k IH] in n |-*; cbn. - - exact I. - - rewrite seq_in. split. lia. apply IH. + intros H1 n k H2 H3. apply H1. apply H1 in H2. lia. Qed. -Fact nat_list_le (A: list nat) n : - (Sigma k, k el A /\ k >= n) + forall k, k el A -> k < n. +Definition segment_sigma : + forall n, Sigma A, length A = n /\ nrep A /\ segment A. Proof. - induction A as [|x A IH]. - - right. easy. - - destruct (le_lt_dec n x) as [H|H]. - + left. exists x. cbn;auto. - + destruct IH as [(k&H1&H2)|H1]. - * left. exists k. cbn. auto. - * right. intros k [<-|H3]; auto. + induction n as [|n (A&IH1&IH2&IH3)]. + - exists []. split. easy. split. easy. apply segment_nil. + - exists (n::A). split; cbn. lia. split. + + split. 2:exact IH2. intros H %IH3. lia. + + intros k. split; cbn. + * intros [<-|H %IH3]; lia. + * intros H. + destruct (nat_eqdec k n) as [->|H1]. now auto. + right. apply IH3. lia. Qed. -Fact nat_list_nrep (A: list nat) n : +Fact segment_nrep A : + segment A -> nrep A. +Proof. + intros H1. + destruct (segment_sigma (length A)) as (B&H2&H3&H4). + eapply nrep_nrep. exact nat_eqdec. exact H3. 2:lia. + apply segment_equal; easy. +Qed. + +Definition nrep_nat_large_el {A: list nat} {n} : nrep A -> length A = S n -> Sigma k, k el A /\ k >= n. Proof. intros H1 H2. - destruct (nat_list_le A n) as [H|H]. exact H. - exfalso. (* computational exfalso *) - enough (length A <= n) by lia. - rewrite <-(seq_length 0 n). - apply nrep_le. exact nat_eqdec. exact H1. - intros k H3. apply seq_in. apply H in H3. lia. + destruct (list_dec (fun k => k >= n) A) as [(x&H3&H4)|H]. + - intros k. + destruct (n-k) eqn:?; unfold dec; intuition lia. + - eauto. + - exfalso. (* computational exfalso *) + destruct (segment_sigma n) as (B&H3&H4&H5). + enough (length A <= length B) by lia. + apply nrep_le. exact nat_eqdec. exact H1. + intros x H6%H. apply H5; lia. +Qed. + +Fact serial_segment A : + serial A -> nrep A -> segment A. +Proof. + intros H1 H2. + destruct (length A) as [|n] eqn:E. + - enough (A = []) as -> by apply segment_nil. + destruct A. easy. cbn in E; lia. + - destruct (nrep_nat_large_el H2 E) as (x&H4&H5). + destruct (segment_sigma (S n)) as (B&H6&H7&H8). + enough (equi A B) as [H9 H10]. + { hnf. hnf in H8. replace (length A) with (length B) by congruence. + firstorder. } + assert (H9: B <<= A). + { intros k H9 %H8. eapply H1. exact H4. lia. } + split. 2:exact H9. + apply nrep_incl. exact nat_eqdec. exact H7. exact H9. lia. +Qed. + + +Fact nat_list_next : + forall A: list nat, Sigma n, forall k, k el A -> k < n. +Proof. + induction A as [|x A [n IH]]. + - exists 0. easy. + - exists (S x + n). intros y [-> |H]. + + lia. + + apply IH in H. lia. Qed. + (*** Exercises: List Reversal *) @@ -914,5 +969,63 @@ Section Reversal. - exact e1. - apply e2, IH. Qed. + + End Reversal. + +(*** Exrcise: seq *) -End Reversal. +Module Saved. +Fixpoint seq n k : list nat := + match k with + 0 => [] + | S k' => n :: seq (S n) k' + end. + +Fact seq_length n k : + length (seq n k) = k. +Proof. + induction k as [|k IH] in n |-*; cbn. + - reflexivity. + - f_equal. apply IH. +Qed. + +Fact seq_in x n k : + x el seq n k <-> n <= x < n + k. +Proof. + induction k as [|k IH] in n |-*; cbn. + - lia. + - rewrite IH. lia. +Qed. + +Fact seq_nrep n k : + nrep (seq n k). +Proof. + induction k as [|k IH] in n |-*; cbn. + - exact I. + - rewrite seq_in. split. lia. apply IH. +Qed. + +Fact nat_list_le (A: list nat) n : + (Sigma k, k el A /\ k >= n) + forall k, k el A -> k < n. +Proof. + induction A as [|x A IH]. + - right. easy. + - destruct (le_lt_dec n x) as [H|H]. + + left. exists x. cbn;auto. + + destruct IH as [(k&H1&H2)|H1]. + * left. exists k. cbn. auto. + * right. intros k [<-|H3]; auto. +Qed. + +Fact nat_list_nrep (A: list nat) n : + nrep A -> length A = S n -> Sigma k, k el A /\ k >= n. +Proof. + intros H1 H2. + destruct (nat_list_le A n) as [H|H]. exact H. + exfalso. (* computational exfalso *) + enough (length A <= n) by lia. + rewrite <-(seq_length 0 n). + apply nrep_le. exact nat_eqdec. exact H1. + intros k H3. apply seq_in. apply H in H3. lia. +Qed. +End Saved. diff --git a/coq/nat.v b/coq/nat.v index 8586a48..2d6b30a 100644 --- a/coq/nat.v +++ b/coq/nat.v @@ -8,7 +8,7 @@ Notation Sig := existT. Notation pi1 := projT1. Notation pi2 := projT2. Notation "'Sigma' x .. y , p" := - (sigT (fun x => .. (sigT (fun y => p)) ..)) + (sigT (fun x => .. (sigT (fun y => p%type)) ..)) (at level 200, x binder, right associativity, format "'[' 'Sigma' '/ ' x .. y , '/ ' p ']'") : type_scope. @@ -332,20 +332,6 @@ Proof. intros H1%le_contra H2%le_contra. eapply le_anti; eassumption. Qed. - -Lemma bounded_forall_dec (p: nat -> Prop) k: - (forall x, dec (p x)) -> dec (forall x, x < k -> p x). -Proof. - intros H. - induction k as [|k IH]. - - left. intros x [=]. - - destruct (H k) as [H1|H1]. - + destruct IH as [IH|IH]; cbn. - * left. intros x H2. - apply le_lt_eq_dec in H2 as [H2| ->]; auto. - * right. contradict IH. intros x H2. apply IH, lt_le, H2. - + right. contradict H1. apply H1, le_refl. -Qed. Fact le_sub x y : x - y <= x. @@ -412,6 +398,63 @@ Proof. - intros [z H]. lia. Qed. +(*** Bounded Quantification *) + +Definition decider {X} (p: X -> Type) := forall x:X, dec (p x). + +Section Bounded. + Variable p: nat -> Type. + Variable d : decider p. + + Definition bounder_sigma_forall n : + (Sigma k, (k <= n) * p k) + (forall k, k <= n -> p k -> False). + Proof. + induction n as [|n [(k&IH1&IH2)|IH]]. + - destruct (d 0) as [H|H]. + + left. exists 0. intuition lia. + + right. intros k H1. assert (k=0) as -> by lia. exact H. + - left. exists k. intuition lia. + - destruct (d (S n)) as [H|H]. + + left. exists (S n). intuition lia. + + right. intros k H1. + destruct (nat_eqdec k (S n)) as [->|H2]. exact H. + apply IH. lia. + Qed. + + Lemma bounded_forall n: + dec (forall k, k <= n -> p k). + Proof. + induction n as [|n [IH|IH]]. + - destruct (d 0) as [H|H]. + + left. intros k H1. assert (k=0) as -> by lia. exact H. + + right. intros H1. apply H, H1. lia. + - destruct (d (S n)) as [H|H]. + + left. intros k H1. + destruct (nat_eqdec k (S n)) as [->|H2]. exact H. + apply IH. lia. + + right. contradict H. apply H. lia. + - right. contradict IH. intros k H. apply IH. lia. + Qed. + + Lemma bounded_sigma n: + dec (Sigma k, (k <= n) * p k). + Proof. + induction n as [|n [(k&IH1&IH2)|IH]]. + - destruct (d 0) as [H|H]. + + left. exists 0. easy. + + right. intros (k&H1&H2). + apply H. assert (k=0) as -> by lia. exact H2. + - left. exists k. intuition lia. + - destruct (d (S n)) as [H|H]. + + left. exists (S n). intuition lia. + + right. + intros (k&H1&H2). + destruct (nat_eqdec k (S n)) as [->|H3]. easy. + apply IH. exists k. intuition lia. + Qed. +End Bounded. + + (*** Complete Induction *) Definition nat_compl_ind (p: nat -> Type) : @@ -461,7 +504,7 @@ Qed. Fact U_Sigma f y : (forall x, f x y = U f x y) -> - forall x, Sigma k, x = k * S y + f x y. + forall x, Sigma k, (x = k * S y + f x y)%nat. Proof. intros H. refine (nat_compl_ind _ _).