• API
• FAQ
• Tools
• Archive
daily pastebin goal
29%
SHARE
TWEET

# Untitled

a guest May 17th, 2018 85 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
1. Set Implicit Arguments.
2.
3. Require Import Omega.
4. Require Import Wf_nat.
5. Require Import Relation_Operators.
6. Require Import Coq.Wellfounded.Lexicographic_Product.
7.
8. (* simultaneously produces a proof of the arith. equation eq and uses it to rewrite in the goal *)
9. Ltac omega_rewrite eq :=
10.   let Hf := fresh in
11.   assert eq as Hf; [omega | rewrite Hf; clear Hf].
12.
13. (* simultaneously produces a proof of the arith. equation eq and uses it to rewrite in H *)
14. Ltac omega_rewrite_ctxt eq H :=
15.   let Hf := fresh in
16.   assert eq as Hf; [omega | rewrite Hf in H; clear Hf].
17.
18. Definition sp_natpair := symprod _ _ lt lt.
19.
20. Lemma wf_pair : well_founded sp_natpair.
21. Proof.
22.   apply wf_symprod; exact lt_wf.
23. Qed.
24.
25. Fixpoint iter{X}(f : X -> X)(n : nat)(x : X) : X :=
26.   match n with
27.   | 0   => x
28.   | S m => f (iter f m x)
29.   end.
30.
31. Lemma iter_plus{X} : forall (f : X -> X)(m n : nat)(x : X), iter f (m + n) x = iter f m (iter f n x).
32. Proof.
33.   intros f m; induction m; intros.
34.   auto.
35.   simpl; congruence.
36. Qed.
37.
38. Lemma iter_S{X} : forall (f : X -> X)(n : nat)(x : X), iter f (S n) x = iter f n (f x).
39. Proof.
40.   intros.
41.   omega_rewrite (S n = n + 1).
42.   rewrite iter_plus; auto.
43. Qed.
44.
45. Definition cyclic{X}(f : X -> X) := forall x x', exists n, iter f n x = x'.
46.
47. Definition inj{X Y}(f : X -> Y) := forall x x', f x = f x' -> x = x'.
48.
49. Lemma iter_aux_lemma : forall (X : Type)(f : X -> X)(x x' y : X)(p : nat * nat),
50.   f x = y -> f x' = y -> iter f (fst p) y = x -> iter f (snd p) y = x' -> x = x'.
51. Proof.
52.   intros X f x x' y p Hx Hx' Hyx Hyx'.
53.   induction (wf_pair p) as [p _ IHp].
54.   destruct p as [m n];  simpl in Hyx,Hyx'.
55.   destruct (dec_eq_nat m n) as [mn_eq | mn_neq].
56.   congruence.
57.   destruct (nat_total_order _ _ mn_neq).
58.   omega_rewrite_ctxt (n = S (pred (n - m)) + m) Hyx'.
59.   rewrite iter_plus, Hyx, iter_S, Hx in Hyx'.
60.   apply (IHp (m, pred (n-m))); [ right; omega | auto | auto ].
61.   omega_rewrite_ctxt (m = S (pred (m - n)) + n) Hyx.
62.   rewrite iter_plus, Hyx', iter_S, Hx' in Hyx.
63.   apply (IHp (pred (m-n), n)); [ left; omega | auto | auto ].
64. Qed.
65.
66. Theorem cyclic_inj : forall (X : Type)(f : X -> X), cyclic f -> inj f.
67. Proof.
68.   intros X f fcyc x x' Hxx'.
69.   destruct (fcyc (f x) x) as [m Hm].
70.   destruct (fcyc (f x) x') as [n Hn].
71.   apply (@iter_aux_lemma _ f _ _ (f x) (m,n)); auto.
72. Qed.
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.

Top