diff options
Diffstat (limited to 'doc/faq/interval_discr.v')
| -rw-r--r-- | doc/faq/interval_discr.v | 419 |
1 files changed, 419 insertions, 0 deletions
diff --git a/doc/faq/interval_discr.v b/doc/faq/interval_discr.v new file mode 100644 index 00000000..972300da --- /dev/null +++ b/doc/faq/interval_discr.v @@ -0,0 +1,419 @@ +(** Sketch of the proof of {p:nat|p<=n} = {p:nat|p<=m} -> n=m + + - preliminary results on the irrelevance of boundedness proofs + - introduce the notion of finite cardinal |A| + - prove that |{p:nat|p<=n}| = n + - prove that |A| = n /\ |A| = m -> n = m if equality is decidable on A + - prove that equality is decidable on A + - conclude +*) + +(** * Preliminary results on [nat] and [le] *) + +(** Proving axiom K on [nat] *) + +Require Import Eqdep_dec. +Require Import Arith. + +Theorem eq_rect_eq_nat : + forall (p:nat) (Q:nat->Type) (x:Q p) (h:p=p), x = eq_rect p Q x p h. +Proof. +intros. +apply K_dec_set with (p := h). +apply eq_nat_dec. +reflexivity. +Qed. + +(** Proving unicity of proofs of [(n<=m)%nat] *) + +Scheme le_ind' := Induction for le Sort Prop. + +Theorem le_uniqueness_proof : forall (n m : nat) (p q : n <= m), p = q. +Proof. +induction p using le_ind'; intro q. + replace (le_n n) with + (eq_rect _ (fun n0 => n <= n0) (le_n n) _ (refl_equal n)). + 2:reflexivity. + generalize (refl_equal n). + pattern n at 2 4 6 10, q; case q; [intro | intros m l e]. + rewrite <- eq_rect_eq_nat; trivial. + contradiction (le_Sn_n m); rewrite <- e; assumption. + replace (le_S n m p) with + (eq_rect _ (fun n0 => n <= n0) (le_S n m p) _ (refl_equal (S m))). + 2:reflexivity. + generalize (refl_equal (S m)). + pattern (S m) at 1 3 4 6, q; case q; [intro Heq | intros m0 l HeqS]. + contradiction (le_Sn_n m); rewrite Heq; assumption. + injection HeqS; intro Heq; generalize l HeqS. + rewrite <- Heq; intros; rewrite <- eq_rect_eq_nat. + rewrite (IHp l0); reflexivity. +Qed. + +(** Proving irrelevance of boundedness proofs while building + elements of interval *) + +Lemma dep_pair_intro : + forall (n x y:nat) (Hx : x<=n) (Hy : y<=n), x=y -> + exist (fun x => x <= n) x Hx = exist (fun x => x <= n) y Hy. +Proof. +intros n x y Hx Hy Heq. +generalize Hy. +rewrite <- Heq. +intros. +rewrite (le_uniqueness_proof x n Hx Hy0). +reflexivity. +Qed. + +(** * Proving that {p:nat|p<=n} = {p:nat|p<=m} -> n=m *) + +(** Definition of having finite cardinality [n+1] for a set [A] *) + +Definition card (A:Set) n := + exists f, + (forall x:A, f x <= n) /\ + (forall x y:A, f x = f y -> x = y) /\ + (forall m, m <= n -> exists x:A, f x = m). + +Require Import Arith. + +(** Showing that the interval [0;n] has cardinality [n+1] *) + +Theorem card_interval : forall n, card {x:nat|x<=n} n. +Proof. +intro n. +exists (fun x:{x:nat|x<=n} => proj1_sig x). +split. +(* bounded *) +intro x; apply (proj2_sig x). +split. +(* injectivity *) +intros (p,Hp) (q,Hq). +simpl. +intro Hpq. +apply dep_pair_intro; assumption. +(* surjectivity *) +intros m Hmn. +exists (exist (fun x : nat => x <= n) m Hmn). +reflexivity. +Qed. + +(** Showing that equality on the interval [0;n] is decidable *) + +Lemma interval_dec : + forall n (x y : {m:nat|m<=n}), {x=y}+{x<>y}. +Proof. +intros n (p,Hp). +induction p; intros ([|q],Hq). +left. + apply dep_pair_intro. + reflexivity. +right. + intro H; discriminate H. +right. + intro H; discriminate H. +assert (Hp' : p <= n). + apply le_Sn_le; assumption. +assert (Hq' : q <= n). + apply le_Sn_le; assumption. +destruct (IHp Hp' (exist (fun m => m <= n) q Hq')) + as [Heq|Hneq]. +left. + injection Heq; intro Heq'. + apply dep_pair_intro. + apply eq_S. + assumption. +right. + intro HeqS. + injection HeqS; intro Heq. + apply Hneq. + apply dep_pair_intro. + assumption. +Qed. + +(** Showing that the cardinality relation is functional on decidable sets *) + +Lemma card_inj_aux : + forall (A:Type) f g n, + (forall x:A, f x <= 0) -> + (forall x y:A, f x = f y -> x = y) -> + (forall m, m <= S n -> exists x:A, g x = m) + -> False. +Proof. +intros A f g n Hfbound Hfinj Hgsurj. +destruct (Hgsurj (S n) (le_n _)) as (x,Hx). +destruct (Hgsurj n (le_S _ _ (le_n _))) as (x',Hx'). +assert (Hfx : 0 = f x). +apply le_n_O_eq. +apply Hfbound. +assert (Hfx' : 0 = f x'). +apply le_n_O_eq. +apply Hfbound. +assert (x=x'). +apply Hfinj. +rewrite <- Hfx. +rewrite <- Hfx'. +reflexivity. +rewrite H in Hx. +rewrite Hx' in Hx. +apply (n_Sn _ Hx). +Qed. + +(** For [dec_restrict], we use a lemma on the negation of equality +that requires proof-irrelevance. It should be possible to avoid this +lemma by generalizing over a first-order definition of [x<>y], say +[neq] such that [{x=y}+{neq x y}] and [~(x=y /\ neq x y)]; for such +[neq], unicity of proofs could be proven *) + + Require Import Classical. + Lemma neq_dep_intro : + forall (A:Set) (z x y:A) (p:x<>z) (q:y<>z), x=y -> + exist (fun x => x <> z) x p = exist (fun x => x <> z) y q. + Proof. + intros A z x y p q Heq. + generalize q; clear q; rewrite <- Heq; intro q. + rewrite (proof_irrelevance _ p q); reflexivity. + Qed. + +Lemma dec_restrict : + forall (A:Set), + (forall x y :A, {x=y}+{x<>y}) -> + forall z (x y :{a:A|a<>z}), {x=y}+{x<>y}. +Proof. +intros A Hdec z (x,Hx) (y,Hy). +destruct (Hdec x y) as [Heq|Hneq]. +left; apply neq_dep_intro; assumption. +right; intro Heq; injection Heq; exact Hneq. +Qed. + +Lemma pred_inj : forall n m, + 0 <> n -> 0 <> m -> pred m = pred n -> m = n. +Proof. +destruct n. +intros m H; destruct H; reflexivity. +destruct m. +intros _ H; destruct H; reflexivity. +simpl; intros _ _ H. +rewrite H. +reflexivity. +Qed. + +Lemma le_neq_lt : forall n m, n <= m -> n<>m -> n < m. +Proof. +intros n m Hle Hneq. +destruct (le_lt_eq_dec n m Hle). +assumption. +contradiction. +Qed. + +Lemma inj_restrict : + forall (A:Set) (f:A->nat) x y z, + (forall x y : A, f x = f y -> x = y) + -> x <> z -> f y < f z -> f z <= f x + -> pred (f x) = f y + -> False. + +(* Search error sans le type de f !! *) +Proof. +intros A f x y z Hfinj Hneqx Hfy Hfx Heq. +assert (f z <> f x). + apply sym_not_eq. + intro Heqf. + apply Hneqx. + apply Hfinj. + assumption. +assert (f x = S (f y)). + assert (0 < f x). + apply le_lt_trans with (f z). + apply le_O_n. + apply le_neq_lt; assumption. + apply pred_inj. + apply O_S. + apply lt_O_neq; assumption. + exact Heq. +assert (f z <= f y). +destruct (le_lt_or_eq _ _ Hfx). + apply lt_n_Sm_le. + rewrite <- H0. + assumption. + contradiction Hneqx. + symmetry. + apply Hfinj. + assumption. +contradiction (lt_not_le (f y) (f z)). +Qed. + +Theorem card_inj : forall m n (A:Set), + (forall x y :A, {x=y}+{x<>y}) -> + card A m -> card A n -> m = n. +Proof. +induction m; destruct n; +intros A Hdec + (f,(Hfbound,(Hfinj,Hfsurj))) + (g,(Hgbound,(Hginj,Hgsurj))). +(* 0/0 *) +reflexivity. +(* 0/Sm *) +destruct (card_inj_aux _ _ _ _ Hfbound Hfinj Hgsurj). +(* Sn/0 *) +destruct (card_inj_aux _ _ _ _ Hgbound Hginj Hfsurj). +(* Sn/Sm *) +destruct (Hgsurj (S n) (le_n _)) as (xSn,HSnx). +rewrite IHm with (n:=n) (A := {x:A|x<>xSn}). +reflexivity. +(* decidability of eq on {x:A|x<>xSm} *) +apply dec_restrict. +assumption. +(* cardinality of {x:A|x<>xSn} is m *) +pose (f' := fun x' : {x:A|x<>xSn} => + let (x,Hneq) := x' in + if le_lt_dec (f xSn) (f x) + then pred (f x) + else f x). +exists f'. +split. +(* f' is bounded *) +unfold f'. +intros (x,_). +destruct (le_lt_dec (f xSn) (f x)) as [Hle|Hge]. +change m with (pred (S m)). +apply le_pred. +apply Hfbound. +apply le_S_n. +apply le_trans with (f xSn). +exact Hge. +apply Hfbound. +split. +(* f' is injective *) +unfold f'. +intros (x,Hneqx) (y,Hneqy) Heqf'. +destruct (le_lt_dec (f xSn) (f x)) as [Hlefx|Hgefx]; +destruct (le_lt_dec (f xSn) (f y)) as [Hlefy|Hgefy]. +(* f xSn <= f x et f xSn <= f y *) +assert (Heq : x = y). + apply Hfinj. + assert (f xSn <> f y). + apply sym_not_eq. + intro Heqf. + apply Hneqy. + apply Hfinj. + assumption. + assert (0 < f y). + apply le_lt_trans with (f xSn). + apply le_O_n. + apply le_neq_lt; assumption. + assert (f xSn <> f x). + apply sym_not_eq. + intro Heqf. + apply Hneqx. + apply Hfinj. + assumption. + assert (0 < f x). + apply le_lt_trans with (f xSn). + apply le_O_n. + apply le_neq_lt; assumption. + apply pred_inj. + apply lt_O_neq; assumption. + apply lt_O_neq; assumption. + assumption. +apply neq_dep_intro; assumption. +(* f y < f xSn <= f x *) +destruct (inj_restrict A f x y xSn); assumption. +(* f x < f xSn <= f y *) +symmetry in Heqf'. +destruct (inj_restrict A f y x xSn); assumption. +(* f x < f xSn et f y < f xSn *) +assert (Heq : x=y). + apply Hfinj; assumption. +apply neq_dep_intro; assumption. +(* f' is surjective *) +intros p Hlep. +destruct (le_lt_dec (f xSn) p) as [Hle|Hlt]. +(* case f xSn <= p *) +destruct (Hfsurj (S p) (le_n_S _ _ Hlep)) as (x,Hx). +assert (Hneq : x <> xSn). + intro Heqx. + rewrite Heqx in Hx. + rewrite Hx in Hle. + apply le_Sn_n with p; assumption. +exists (exist (fun a => a<>xSn) x Hneq). +unfold f'. +destruct (le_lt_dec (f xSn) (f x)) as [Hle'|Hlt']. +rewrite Hx; reflexivity. +rewrite Hx in Hlt'. +contradiction (le_not_lt (f xSn) p). +apply lt_trans with (S p). +apply lt_n_Sn. +assumption. +(* case p < f xSn *) +destruct (Hfsurj p (le_S _ _ Hlep)) as (x,Hx). +assert (Hneq : x <> xSn). + intro Heqx. + rewrite Heqx in Hx. + rewrite Hx in Hlt. + apply (lt_irrefl p). + assumption. +exists (exist (fun a => a<>xSn) x Hneq). +unfold f'. +destruct (le_lt_dec (f xSn) (f x)) as [Hle'|Hlt']. + rewrite Hx in Hle'. + contradiction (lt_irrefl p). + apply lt_le_trans with (f xSn); assumption. + assumption. +(* cardinality of {x:A|x<>xSn} is n *) +pose (g' := fun x' : {x:A|x<>xSn} => + let (x,Hneq) := x' in + if Hdec x xSn then 0 else g x). +exists g'. +split. +(* g is bounded *) +unfold g'. +intros (x,_). +destruct (Hdec x xSn) as [_|Hneq]. +apply le_O_n. +assert (Hle_gx:=Hgbound x). +destruct (le_lt_or_eq _ _ Hle_gx). +apply lt_n_Sm_le. +assumption. +contradiction Hneq. +apply Hginj. +rewrite HSnx. +assumption. +split. +(* g is injective *) +unfold g'. +intros (x,Hneqx) (y,Hneqy) Heqg'. +destruct (Hdec x xSn) as [Heqx|_]. +contradiction Hneqx. +destruct (Hdec y xSn) as [Heqy|_]. +contradiction Hneqy. +assert (Heq : x=y). + apply Hginj; assumption. +apply neq_dep_intro; assumption. +(* g is surjective *) +intros p Hlep. +destruct (Hgsurj p (le_S _ _ Hlep)) as (x,Hx). +assert (Hneq : x<>xSn). + intro Heq. + rewrite Heq in Hx. + rewrite Hx in HSnx. + rewrite HSnx in Hlep. + contradiction (le_Sn_n _ Hlep). +exists (exist (fun a => a<>xSn) x Hneq). +simpl. +destruct (Hdec x xSn) as [Heqx|_]. +contradiction Hneq. +assumption. +Qed. + +(** Conclusion *) + +Theorem interval_discr : + forall n m, {p:nat|p<=n} = {p:nat|p<=m} -> n=m. +Proof. +intros n m Heq. +apply card_inj with (A := {p:nat|p<=n}). +apply interval_dec. +apply card_interval. +rewrite Heq. +apply card_interval. +Qed. |