Lemma dupfree_injective_map (X Y:Type) (f: X -> Y) (L : list X) : dupfree L -> injective f -> dupfree (map f L).
Proof.
intros D Inj. induction D as [| x A]; simpl; constructor.
- intros [y [E1 E2]] % in_map_iff. apply Inj in E1. now subst y.
- apply IHD.
Qed.
Finite type {n|n<=k}
This is not the most beautiest code since it is obvious that this is a finite type
Construct the list of all numbers <= k
Definition le_k k := fun n => n <= k.
Instance dec_le_k k n : dec ( le_k k n). Proof. auto. Defined.
Definition Le_K k := {n | (pure (le_k k)) n}.
Instance dec_pure_le_k k n : dec (pure (le_k k) n).
Proof.
apply dec_trans with (P:= le_k k n); auto using pure_equiv.
Qed.
Hint Resolve dec_pure_le_k.
Lemma pure_le_k_iff k n : n <= k <-> pure (le_k k) n.
Proof.
rewrite <-pure_equiv. unfold le_k. tauto.
Qed.
Definition upgrade_bound k (x: Le_K k): Le_K (S k).
Proof.
destruct x as [n L]. exists n. apply pure_le_k_iff. constructor. now apply pure_le_k_iff.
Defined.
Definition id_Le_K k : Le_K k.
Proof.
exists k. apply pure_le_k_iff. constructor.
Defined.
Definition create_Le_K k n: n <= k -> Le_K k.
Proof.
intros L. exists n. now apply pure_le_k_iff.
Defined.
Fixpoint nums_leq_K (k : nat) : list (Le_K k) :=
match k with
| 0 => [id_Le_K 0]
| S k => id_Le_K (S k) :: map (upgrade_bound (k:=k)) (nums_leq_K k)
end.
Lemma nums_leq_K_complete k (x:Le_K k ) : x el (nums_leq_K k).
Proof.
induction k; destruct x as [n L].
- cbn. left. unfold id_Le_K.
assert(n = 0). { apply pure_le_k_iff in L. omega. } subst n.
f_equal. apply pure_eq.
- decide (n = S k) as [-> |D]; cbn.
+ left. unfold id_Le_K. f_equal. apply pure_eq.
+ right. apply in_map_iff.
assert (n <= k) as H. { apply pure_le_k_iff in L. omega. }
exists (create_Le_K H). split.
* unfold upgrade_bound. cbn. f_equal. apply pure_eq.
* apply IHk.
Qed.
Lemma nums_leq_K_dupfree k: dupfree (nums_leq_K k).
Proof.
induction k; cbn; constructor; auto.
- constructor.
- intros [[n L] [E1 E2]] % in_map_iff. enough (n = S k).
+ clear E1 E2. apply pure_le_k_iff in L. omega.
+ unfold upgrade_bound, id_Le_K in E1. congruence.
- apply dupfree_injective_map.
+ apply IHk.
+ intros [n1 L1] [n2 L2]. unfold upgrade_bound. intros L.
assert (n1 = n2) by congruence. subst n2. f_equal. apply pure_eq.
Qed.
Instance LE_K_eq_dec k : eq_dec (Le_K k).
Proof.
intros [n1 p1] [n2 p2].
decide (n1 = n2) as [<- |D].
- left. f_equal. now apply pure_eq.
- right. congruence.
Defined.
Canonical Structure EqLe_K k := EqType (Le_K k).
Lemma Le_K_enum_ok k (x : EqLe_K k) : count (X:= EqLe_K k) (nums_leq_K k) x =1.
Proof.
apply dupfreeCount.
- apply nums_leq_K_dupfree.
- apply nums_leq_K_complete.
Qed.
Instance finTypeC_Le_K k: finTypeC (EqLe_K k).
Proof.
econstructor. apply Le_K_enum_ok.
Defined.
Canonical Structure finType_Le_K k: finType := FinType (EqLe_K k).
Cardinality is S k
Lemma nums_leq_K_length k : length (nums_leq_K k) = S k.
Proof.
induction k.
- now cbn.
- cbn. now rewrite map_length, IHk.
Qed.
Lemma card_finTypeC_Le_K k : length(enum (finTypeC := finTypeC_Le_K k )) = S k.
Proof.
unfold finType_Le_K. cbn.
now apply nums_leq_K_length.
Qed.
Lemma card_finType_Le_K k : Cardinality( finType_Le_K k ) = S k.
Proof.
unfold Cardinality. apply card_finTypeC_Le_K.
Qed.
Lemma le_L_is_le k (N : finType_Le_K k): proj1_sig N <= k.
Proof.
destruct N. cbn. now apply pure_le_k_iff.
Qed.
End FirstKFinType.
Decisions for this Type
Instance bounded_type_exist k (P: (Le_K k) -> Prop) (decP: forall L, dec (P L)): dec( exists L, P L).
Proof. auto. Qed.
Instance bounded_forall k (P:nat -> Prop) (decP: forall n, dec (P n)): dec(forall n, n <= k -> P (n)).
Proof.
pose (P' := fun (n:Le_K k) => P (proj1_sig n)).
enough (dec (forall (n:Le_K k), P' n)) as [H|H].
- left. intros n L. apply (H (create_Le_K L)).
- right. intros N. apply H. intros [n L]. apply N. cbn. now apply pure_le_k_iff.
- auto.
Qed.
Instance bounded_exist k (P:nat -> Prop) (decP: forall n, dec (P n)): dec(exists n, n <= k /\ P (n)).
Proof.
pose (P' := fun (n:Le_K k) => P (proj1_sig n)).
enough (dec (exists (n:Le_K k), P' n)) as [H|H].
- left. destruct H as [[n p] Pn]. exists n. split; auto.
now apply pure_le_k_iff.
- right. intros [n [L Pn]].
apply H. now exists (create_Le_K L).
- auto.
Qed.
Instance bounded_strict_forall k (P:nat -> Prop) (decP: forall n, dec (P n)): dec(forall n, n < k -> P (n)).
Proof.
destruct k.
- left. intros n L. exfalso. omega.
- apply dec_trans with (P:= forall n, n <= k -> P n); auto.
split; intros Q n L; apply Q; omega.
Qed.
Instance strict_bounded_exist k (P:nat -> Prop) (decP: forall n, dec (P n)): dec(exists n, n < k /\ P (n)).
Proof.
destruct k.
- right. intros [n [L _]]. omega.
- apply dec_trans with (P:= exists n, n <= k /\ P n); auto.
split; intros [n [L Q]]; exists n; split; oauto.
Qed.
Instance dec_pure_le_k_public x y : dec (pure (le_k x) y).
Proof. apply dec_pure_le_k. Defined.
Hint Resolve dec_pure_le_k_public. (* The other does not work for some reasons even it is registered*)
Lemma list_eq (X: Type) (l1 l2: list X) : (forall n, nth_error l1 n= nth_error l2 n) -> l1 = l2.
Proof.
revert l2. induction l1; intros l2 EE.
- specialize (EE 0). cbn in EE. now destruct l2.
- destruct l2.
+ now specialize (EE 0).
+ f_equal.
* specialize (EE 0). cbn in EE. congruence.
* apply IHl1.
intros n. specialize (EE (S n)). now cbn in EE.
Qed.
Notation "A ^^ l" := (A^(finType_fromList l)) (at level 30).
Section Vectors.
Lemma vector_eq (X Y: finType) (a b : X^Y) : (forall y, applyVect a y = applyVect b y) -> a = b.
Proof.
intros E.
apply vector_extensionality.
rewrite <-(vectorise_apply_inverse a).
rewrite <-(vectorise_apply_inverse b). cbn.
unfold getImage. apply list_eq.
induction (elem Y); intros n; cbn; auto.
destruct n; cbn; auto using IHl. now f_equal.
Qed.
Context {B:finType}.
Context {C:eqType}.
Definition toFinTypeFromList (L:list C)(x:C) (E: x el L) : (finType_fromList L) :=
exist (pure (fun x => x el L)) x (match (pure_equiv (p:= fun x => x el L) x) with conj P _ => P E end).
Definition fromFinTypeFromList (L:list C) (l:finType_fromList L) : C := match l with
| exist _ x P => x end.
Lemma toFinTypeFromListEq (L : list C) (x:C) (E1: x el L) (E2: x el L) : toFinTypeFromList E1 = toFinTypeFromList E2.
Proof.
unfold toFinTypeFromList. f_equal. destruct pure_equiv. apply pure_eq.
Qed.
Lemma from_to_fin_type_from_list (L : list C) (x:C) (E: x el L): x = (fromFinTypeFromList (toFinTypeFromList E)).
Proof.
reflexivity.
Qed.
Section Narrowing.
Context {l_1 l_2 : list C}.
Variable (P: l_1 <<= l_2).
Definition narrowVector: B^^l_2 -> B^^l_1.
Proof.
intros v. apply vectorise. intros [a Q]. apply (applyVect v).
exists a. apply pure_equiv in Q. now apply pure_equiv, P.
Defined.
Lemma narrowVectorCorrect c (M_1:c el l_1) (M_2:c el l_2) v: applyVect v (toFinTypeFromList M_2) = applyVect (narrowVector v) (toFinTypeFromList M_1).
Proof.
unfold narrowVector, toFinTypeFromList.
rewrite apply_vectorise_inverse. f_equal. f_equal. apply pure_eq.
Qed.
End Narrowing.
Context{l:list C} (c:C).
Implicit Types (b:B)(c:C).
Lemma rem_sub : rem l c <<= l. Proof. auto. Qed.
Definition separate : B ^^l -> B ^^(rem l c) := narrowVector rem_sub.
Definition rest (M: c el l) : B ^^l -> B.
Proof.
intros Z. apply (applyVect Z). exists c. now apply pure_equiv.
Defined.
Definition join : (B ^^ (rem l c))*B -> B ^^l.
Proof.
intros [Z x]. apply vectorise. intros [y P]. decide (y = c).
- exact x.
- apply (applyVect Z). exists y. apply pure_equiv in P. now apply pure_equiv, in_rem_iff.
Defined.
Lemma join_fst (M: c el l)(v: B ^^ (rem l c)) b : applyVect (join (v, b)) (toFinTypeFromList M) = b.
Proof.
unfold join, toFinTypeFromList. cbn. rewrite apply_vectorise_inverse. now destruct decision; (try (now exfalso; auto)).
Qed.
Lemma join_snd (v: B ^^ (rem l c)) b c' (Q: c' el l) (Q': c' el (rem l c)): applyVect (join (v, b)) (toFinTypeFromList Q) = applyVect v (toFinTypeFromList Q').
Proof.
unfold join, toFinTypeFromList. cbn. rewrite apply_vectorise_inverse. destruct decision.
- exfalso. subst c'. apply in_rem_iff in Q'. tauto.
- f_equal. f_equal. apply pure_eq.
Qed.
Lemma inv_separate_join Z b: separate(join (Z, b)) = Z.
Proof.
unfold separate,join, narrowVector. destruct Z as [x Z]. apply vector_eq. intros [y P].
rewrite !apply_vectorise_inverse. destruct decision.
- exfalso. apply pure_equiv in P. now apply in_rem_iff in P.
- f_equal. f_equal. apply pure_eq.
Qed.
Lemma inv_join_separate (M: c el l) Z : join ( (separate Z ), (rest M Z)) = Z.
Proof.
unfold separate,join, rest, narrowVector. apply vector_eq. intros [x P].
rewrite apply_vectorise_inverse. destruct decision as [<- |D].
- repeat f_equal. apply pure_eq.
- rewrite apply_vectorise_inverse. repeat f_equal. apply pure_eq.
Qed.
Section ConvertRemNotIn.
Variable (M: ~ c el l).
Lemma rem_not_in_eq: l <<= rem l c.
Proof. auto. Qed.
Definition convRemInv : B ^^ (rem l c) -> B^^l := narrowVector (rem_not_in_eq).
Lemma convRemInv_correct Z c' (Y: c' el l) (Y': c' el (rem l c)) : applyVect Z (toFinTypeFromList Y') = applyVect (convRemInv Z) (toFinTypeFromList Y).
Proof.
unfold convRemInv. now rewrite <-narrowVectorCorrect with (M_2 := Y').
Qed.
Lemma convRemInv_correct' Z: convRemInv (separate Z) = Z.
Proof.
unfold convRemInv, separate, narrowVector. apply vector_eq. intros [y P].
rewrite !apply_vectorise_inverse. repeat f_equal. apply pure_eq.
Qed.
Lemma separate_unchanged Z: separate (convRemInv Z) = Z.
Proof.
unfold convRemInv, separate, narrowVector. apply vector_eq. intros [y P].
rewrite !apply_vectorise_inverse. repeat f_equal. apply pure_eq.
Qed.
End ConvertRemNotIn.
End Vectors.
Section Quotients.
Context (X:finType).
Variable (E: X -> X -> Prop).
Variable (EisEquiv: Equivalence E).
Context {decP : forall x y, dec (E x y)}.
Instance EisEquivProper: Equivalence E. Proof. apply EisEquiv. Qed.
Fixpoint get_equiv_class_rep x (L: list X) := match L with
| [] => x
| y::L => if (decision (E y x)) then y else (get_equiv_class_rep x L) end.
Lemma get_equiv_class_rep_equiv x L : E (get_equiv_class_rep x L) x.
Proof.
induction L; cbn.
- reflexivity.
- destruct decision as [D|D]; auto.
Qed.
Lemma get_equiv_class_rep_less x y L : y el L -> getPosition L y < getPosition L (get_equiv_class_rep x L) -> ~ E (get_equiv_class_rep x L) y.
Proof.
intros In Leq Equiv. induction L.
- now exfalso.
- cbn in *. decide (y = a).
+ subst a. cbn in *. trivial_decision. destruct decision as [D'|D'] in Equiv.
* rewrite decision_true in Leq. omega.
now rewrite decision_true.
* apply D'. rewrite get_equiv_class_rep_equiv in Equiv. now symmetry.
+ apply IHL.
* destruct In as [Eq |In]. exfalso. auto. assumption.
* decide (E a x).
-- trivial_decision. exfalso. omega.
-- destruct decision in Leq.
++ exfalso. omega.
++ omega.
* decide (E a x).
-- trivial_decision. exfalso. omega.
-- assumption.
Qed.
Lemma get_equiv_class_rep_unique x y L : x el L -> y el L -> E x y -> (get_equiv_class_rep x L) = (get_equiv_class_rep y L).
Proof.
intros InX InY Equiv. induction L.
- now exfalso.
- cbn. decide (E a x) as [D|D].
+ rewrite decision_true. reflexivity. now rewrite D.
+ rewrite decision_false. apply IHL.
* destruct InX; auto.
exfalso. subst x. apply D. reflexivity.
* destruct InY; auto.
exfalso. subst a. apply D. now symmetry.
* intros Equiv'. apply D. now rewrite Equiv.
Qed.
Instance dec_smallest x : dec (forall y, #y < #x -> ~E x y).
Proof. auto. Qed.
Definition equiv_class : finType := finType_sub (fun x => forall y, #y < #x -> ~E x y) dec_smallest.
Definition in_equiv_class (C: equiv_class) y := match C with exist _ x _ => E x y end.
Definition get_equiv_class (x:X) : equiv_class.
Proof.
exists (get_equiv_class_rep x (elem X)).
apply pure_equiv. intros y L.
apply get_equiv_class_rep_less; auto.
Defined.
Lemma get_equiv_class_correct x : in_equiv_class (get_equiv_class x) x.
Proof.
unfold get_equiv_class, in_equiv_class. apply get_equiv_class_rep_equiv.
Qed.
End Quotients.
Proof.
revert l2. induction l1; intros l2 EE.
- specialize (EE 0). cbn in EE. now destruct l2.
- destruct l2.
+ now specialize (EE 0).
+ f_equal.
* specialize (EE 0). cbn in EE. congruence.
* apply IHl1.
intros n. specialize (EE (S n)). now cbn in EE.
Qed.
Notation "A ^^ l" := (A^(finType_fromList l)) (at level 30).
Section Vectors.
Lemma vector_eq (X Y: finType) (a b : X^Y) : (forall y, applyVect a y = applyVect b y) -> a = b.
Proof.
intros E.
apply vector_extensionality.
rewrite <-(vectorise_apply_inverse a).
rewrite <-(vectorise_apply_inverse b). cbn.
unfold getImage. apply list_eq.
induction (elem Y); intros n; cbn; auto.
destruct n; cbn; auto using IHl. now f_equal.
Qed.
Context {B:finType}.
Context {C:eqType}.
Definition toFinTypeFromList (L:list C)(x:C) (E: x el L) : (finType_fromList L) :=
exist (pure (fun x => x el L)) x (match (pure_equiv (p:= fun x => x el L) x) with conj P _ => P E end).
Definition fromFinTypeFromList (L:list C) (l:finType_fromList L) : C := match l with
| exist _ x P => x end.
Lemma toFinTypeFromListEq (L : list C) (x:C) (E1: x el L) (E2: x el L) : toFinTypeFromList E1 = toFinTypeFromList E2.
Proof.
unfold toFinTypeFromList. f_equal. destruct pure_equiv. apply pure_eq.
Qed.
Lemma from_to_fin_type_from_list (L : list C) (x:C) (E: x el L): x = (fromFinTypeFromList (toFinTypeFromList E)).
Proof.
reflexivity.
Qed.
Section Narrowing.
Context {l_1 l_2 : list C}.
Variable (P: l_1 <<= l_2).
Definition narrowVector: B^^l_2 -> B^^l_1.
Proof.
intros v. apply vectorise. intros [a Q]. apply (applyVect v).
exists a. apply pure_equiv in Q. now apply pure_equiv, P.
Defined.
Lemma narrowVectorCorrect c (M_1:c el l_1) (M_2:c el l_2) v: applyVect v (toFinTypeFromList M_2) = applyVect (narrowVector v) (toFinTypeFromList M_1).
Proof.
unfold narrowVector, toFinTypeFromList.
rewrite apply_vectorise_inverse. f_equal. f_equal. apply pure_eq.
Qed.
End Narrowing.
Context{l:list C} (c:C).
Implicit Types (b:B)(c:C).
Lemma rem_sub : rem l c <<= l. Proof. auto. Qed.
Definition separate : B ^^l -> B ^^(rem l c) := narrowVector rem_sub.
Definition rest (M: c el l) : B ^^l -> B.
Proof.
intros Z. apply (applyVect Z). exists c. now apply pure_equiv.
Defined.
Definition join : (B ^^ (rem l c))*B -> B ^^l.
Proof.
intros [Z x]. apply vectorise. intros [y P]. decide (y = c).
- exact x.
- apply (applyVect Z). exists y. apply pure_equiv in P. now apply pure_equiv, in_rem_iff.
Defined.
Lemma join_fst (M: c el l)(v: B ^^ (rem l c)) b : applyVect (join (v, b)) (toFinTypeFromList M) = b.
Proof.
unfold join, toFinTypeFromList. cbn. rewrite apply_vectorise_inverse. now destruct decision; (try (now exfalso; auto)).
Qed.
Lemma join_snd (v: B ^^ (rem l c)) b c' (Q: c' el l) (Q': c' el (rem l c)): applyVect (join (v, b)) (toFinTypeFromList Q) = applyVect v (toFinTypeFromList Q').
Proof.
unfold join, toFinTypeFromList. cbn. rewrite apply_vectorise_inverse. destruct decision.
- exfalso. subst c'. apply in_rem_iff in Q'. tauto.
- f_equal. f_equal. apply pure_eq.
Qed.
Lemma inv_separate_join Z b: separate(join (Z, b)) = Z.
Proof.
unfold separate,join, narrowVector. destruct Z as [x Z]. apply vector_eq. intros [y P].
rewrite !apply_vectorise_inverse. destruct decision.
- exfalso. apply pure_equiv in P. now apply in_rem_iff in P.
- f_equal. f_equal. apply pure_eq.
Qed.
Lemma inv_join_separate (M: c el l) Z : join ( (separate Z ), (rest M Z)) = Z.
Proof.
unfold separate,join, rest, narrowVector. apply vector_eq. intros [x P].
rewrite apply_vectorise_inverse. destruct decision as [<- |D].
- repeat f_equal. apply pure_eq.
- rewrite apply_vectorise_inverse. repeat f_equal. apply pure_eq.
Qed.
Section ConvertRemNotIn.
Variable (M: ~ c el l).
Lemma rem_not_in_eq: l <<= rem l c.
Proof. auto. Qed.
Definition convRemInv : B ^^ (rem l c) -> B^^l := narrowVector (rem_not_in_eq).
Lemma convRemInv_correct Z c' (Y: c' el l) (Y': c' el (rem l c)) : applyVect Z (toFinTypeFromList Y') = applyVect (convRemInv Z) (toFinTypeFromList Y).
Proof.
unfold convRemInv. now rewrite <-narrowVectorCorrect with (M_2 := Y').
Qed.
Lemma convRemInv_correct' Z: convRemInv (separate Z) = Z.
Proof.
unfold convRemInv, separate, narrowVector. apply vector_eq. intros [y P].
rewrite !apply_vectorise_inverse. repeat f_equal. apply pure_eq.
Qed.
Lemma separate_unchanged Z: separate (convRemInv Z) = Z.
Proof.
unfold convRemInv, separate, narrowVector. apply vector_eq. intros [y P].
rewrite !apply_vectorise_inverse. repeat f_equal. apply pure_eq.
Qed.
End ConvertRemNotIn.
End Vectors.
Section Quotients.
Context (X:finType).
Variable (E: X -> X -> Prop).
Variable (EisEquiv: Equivalence E).
Context {decP : forall x y, dec (E x y)}.
Instance EisEquivProper: Equivalence E. Proof. apply EisEquiv. Qed.
Fixpoint get_equiv_class_rep x (L: list X) := match L with
| [] => x
| y::L => if (decision (E y x)) then y else (get_equiv_class_rep x L) end.
Lemma get_equiv_class_rep_equiv x L : E (get_equiv_class_rep x L) x.
Proof.
induction L; cbn.
- reflexivity.
- destruct decision as [D|D]; auto.
Qed.
Lemma get_equiv_class_rep_less x y L : y el L -> getPosition L y < getPosition L (get_equiv_class_rep x L) -> ~ E (get_equiv_class_rep x L) y.
Proof.
intros In Leq Equiv. induction L.
- now exfalso.
- cbn in *. decide (y = a).
+ subst a. cbn in *. trivial_decision. destruct decision as [D'|D'] in Equiv.
* rewrite decision_true in Leq. omega.
now rewrite decision_true.
* apply D'. rewrite get_equiv_class_rep_equiv in Equiv. now symmetry.
+ apply IHL.
* destruct In as [Eq |In]. exfalso. auto. assumption.
* decide (E a x).
-- trivial_decision. exfalso. omega.
-- destruct decision in Leq.
++ exfalso. omega.
++ omega.
* decide (E a x).
-- trivial_decision. exfalso. omega.
-- assumption.
Qed.
Lemma get_equiv_class_rep_unique x y L : x el L -> y el L -> E x y -> (get_equiv_class_rep x L) = (get_equiv_class_rep y L).
Proof.
intros InX InY Equiv. induction L.
- now exfalso.
- cbn. decide (E a x) as [D|D].
+ rewrite decision_true. reflexivity. now rewrite D.
+ rewrite decision_false. apply IHL.
* destruct InX; auto.
exfalso. subst x. apply D. reflexivity.
* destruct InY; auto.
exfalso. subst a. apply D. now symmetry.
* intros Equiv'. apply D. now rewrite Equiv.
Qed.
Instance dec_smallest x : dec (forall y, #y < #x -> ~E x y).
Proof. auto. Qed.
Definition equiv_class : finType := finType_sub (fun x => forall y, #y < #x -> ~E x y) dec_smallest.
Definition in_equiv_class (C: equiv_class) y := match C with exist _ x _ => E x y end.
Definition get_equiv_class (x:X) : equiv_class.
Proof.
exists (get_equiv_class_rep x (elem X)).
apply pure_equiv. intros y L.
apply get_equiv_class_rep_less; auto.
Defined.
Lemma get_equiv_class_correct x : in_equiv_class (get_equiv_class x) x.
Proof.
unfold get_equiv_class, in_equiv_class. apply get_equiv_class_rep_equiv.
Qed.
End Quotients.