daily pastebin goal
67%
SHARE
TWEET

Untitled

a guest May 17th, 2018 84 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. OK, I Understand
 
Top