Part of Slepp's ProjectsPastebinTURLImagebinFilebin
Feedback -- English French German Japanese
Create Upload Newest Tools Donate
Sign In | Create Account

Miscellany
Monday, February 4th, 2013 at 8:50:18pm UTC 

  1. Require Import Coq.Arith.Le.
  2. Require Import Coq.Lists.List.
  3. Require Import Coq.Setoids.Setoid.
  4.  
  5. Lemma EIAK : forall p1 : Prop, False -> p1 <-> True.
  6. Proof. tauto. Qed.
  7.  
  8. Lemma FXAF : forall p1 : Prop, p1 -> True <-> True.
  9. Proof. tauto. Qed.
  10.  
  11. Lemma NPUA : forall p1 : Prop, True -> p1 <-> p1.
  12. Proof. tauto. Qed.
  13.  
  14. Hint Rewrite EIAK FXAF NPUA : Hints.
  15.  
  16. Lemma YQHC : forall p1, (p1 <-> p1) <-> True.
  17. Proof. tauto. Qed.
  18.  
  19. Lemma RLKE : forall p1, (p1 <-> True) <-> p1.
  20. Proof. tauto. Qed.
  21.  
  22. Lemma MQOS : forall p1, (True <-> p1) <-> p1.
  23. Proof. tauto. Qed.
  24.  
  25. Hint Rewrite YQHC RLKE MQOS : Hints.
  26.  
  27. Lemma GEKE : forall p1, p1 /\ True <-> p1.
  28. Proof. tauto. Qed.
  29.  
  30. Lemma VKBY : forall p1, True /\ p1 <-> p1.
  31. Proof. tauto. Qed.
  32.  
  33. Hint Rewrite GEKE VKBY : Hints.
  34.  
  35. Lemma ATGO : forall (t1 : Type) (o1 : t1), o1 = o1 <-> True.
  36. Proof. tauto. Qed.
  37.  
  38. Lemma RNCR : forall (t1 : Type) (o1 : t1), o1 <> o1 <-> False.
  39. Proof. tauto. Qed.
  40.  
  41. Hint Rewrite ATGO RNCR : Hints.
  42.  
  43. Lemma YPTZ : forall n1, O = S n1 <-> False.
  44. Proof. intro n1; split; intro H1; inversion H1. Qed.
  45.  
  46. Lemma NYAI : forall n1, S n1 = O <-> False.
  47. Proof. intro n1; split; intro H1; inversion H1. Qed.
  48.  
  49. Lemma USIJ : forall n1 n2, S n1 = S n2 <-> n1 = n2.
  50. Proof. auto with *. Qed.
  51.  
  52. Hint Rewrite YPTZ NYAI USIJ : Hints.
  53.  
  54. Lemma UNIX : forall n1, n1 <= n1 <-> True.
  55. Proof. auto with *. Qed.
  56.  
  57. Lemma YQUL : forall n1, O <= S n1 <-> True.
  58. Proof. auto with *. Qed.
  59.  
  60. Lemma EUTT : forall n1, S n1 <= O <-> False.
  61. Proof.
  62. intro n1.
  63. split.
  64.   apply le_Sn_O.
  65.  
  66.   tauto.
  67. Qed.
  68.  
  69. Lemma HYAZ : forall n1 n2, S n1 <= S n2 <-> n1 <= n2.
  70. Proof. auto with *. Qed.
  71.  
  72. Lemma HTQF : forall n1, O <= n1 <-> True.
  73. Proof. auto with *. Qed.
  74.  
  75. Lemma NNQD : forall n1, n1 <= S n1 <-> True.
  76. Proof. auto with *. Qed.
  77.  
  78. Hint Rewrite UNIX YQUL EUTT HYAZ HTQF NNQD : Hints.
  79.  
  80. Lemma VTCJ : false = true <-> False.
  81. Proof. intuition. Qed.
  82.  
  83. Lemma GLHY : true = false <-> False.
  84. Proof. intuition. Qed.
  85.  
  86. Hint Rewrite VTCJ GLHY : Hints.
  87.  
  88. Parameter A:Type.
  89.  
  90. Parameter  var_dec : forall (x y : A),{x=y}+{~x=y}.
  91.  
  92. Lemma OVGF : forall (t1 : Type) (a : t1), In a nil <-> False.
  93. Proof. tauto. Qed.
  94.  
  95. Lemma FPIU : forall (t1 : Type) (a b : t1) (l1 : list t1), In a (b :: l1) <-> a = b \/ In a l1.
  96. Proof. intros t1 a b l1. unfold In. intuition. Qed.
  97.  
  98. Hint Rewrite OVGF FPIU : Hints.
  99.  
  100. Definition included (l1 l2:list A):Prop :=
  101.               forall x:A,In x l1 -> In x l2.
  102.  
  103. Lemma NOMZ : forall l1 l2, included l1 l2 <-> forall x:A,In x l1 -> In x l2.
  104. Proof. tauto. Qed.
  105.  
  106. Hint Rewrite NOMZ : Hints.
  107.  
  108. Fixpoint inbool (x:A) (l:list A) :bool :=
  109.            match l with
  110.            | nil => false
  111.            | x'::l' => match (var_dec x' x) with
  112.                            | left _ => true
  113.                            | right _ => inbool x l'
  114.                            end
  115.            end.
  116.  
  117. Lemma inbool_def_1 : forall a, inbool a nil = false.
  118. Proof. trivial. Qed.
  119.  
  120. Lemma inbool_def_2 : forall a b l1, a = b -> inbool a (b :: l1) = true.
  121. Proof. intros a b l1 H1; simpl; destruct (var_dec b a); congruence. Qed.
  122.  
  123. Lemma inbool_def_3 : forall a b l1, a <> b -> inbool a (b :: l1) = inbool a l1.
  124. Proof. intros a b l1 H1; simpl; destruct (var_dec b a); congruence. Qed.
  125.  
  126. Hint Rewrite inbool_def_1 : Hints.
  127.  
  128. Hint Rewrite inbool_def_2 inbool_def_3 using autorewrite with Hints; congruence : Hints.
  129.  
  130. Lemma KIDZ : forall l1, included nil l1 <-> True.
  131. Proof.
  132. intro l1.
  133. split.
  134.   autorewrite with Hints.
  135.   auto.
  136.  
  137.   autorewrite with Hints.
  138.   intro x.
  139.   autorewrite with Hints.
  140.   tauto.
  141. Qed.
  142.  
  143. Hint Rewrite KIDZ : Hints.
  144.  
  145. Fixpoint diff(l1 l2:list A):nat :=
  146.   match l2 with
  147.   | nil => 0
  148.   | x::l' => if inbool x l1 then diff l1 l' else S (diff (x::l1) l')
  149.   end.
  150.  
  151. Lemma diff_def_1 : forall l1, diff l1 nil = O.
  152. Proof. trivial. Qed.
  153.  
  154. Lemma diff_def_2 : forall a l1 l2, inbool a l1 = true -> diff l1 (a :: l2) = diff l1 l2.
  155. Proof. intros a l1 l2 H1; simpl; rewrite H1; trivial. Qed.
  156.  
  157. Lemma diff_def_3 : forall a l1 l2, inbool a l1 = false -> diff l1 (a :: l2) = S (diff (a :: l1) l2).
  158. Proof. intros a l1 l2 H1; simpl; rewrite H1; trivial. Qed.
  159.  
  160. Hint Rewrite diff_def_1 : Hints.
  161.  
  162. Hint Rewrite diff_def_2 diff_def_3 using autorewrite with Hints; tauto : Hints.
  163.  
  164. Lemma diff_simpl : forall l1, ((forall l2 a, inbool a l1 = false -> inbool a l2 = false -> diff (a :: l2) l1 = diff l2 l1) /\ (forall l2 a, inbool a l1 = false -> inbool a l2 = true -> diff (a :: l2) l1 = diff l2 l1)) /\ (forall l2 a, inbool a l1 = true -> inbool a l2 = false -> S (diff (a :: l2) l1) = diff l2 l1) /\ (forall l2 a, inbool a l1 = true -> inbool a l2 = true -> diff (a :: l2) l1 = diff l2 l1).
  165. Proof.
  166. induction l1 as [| b l1 IH1];
  167.   split;
  168.     split;
  169.       intros l2 a H1 H2;
  170.       try (
  171.           remember (inbool b l1) as b1;
  172.           symmetry in Heqb1;
  173.           destruct b1);
  174.         try (
  175.             remember (inbool b l2) as b2;
  176.             symmetry in Heqb2;
  177.             destruct b2);
  178.           try (
  179.               assert (H3 := var_dec a b);
  180.               destruct H3 as [H3 | H3]);
  181.             try (destruct IH1 as [[IH1 IH2] [IH3 IH4]]);
  182.               autorewrite with Hints in H1;
  183.               autorewrite with Hints in H2;
  184.               try (autorewrite with Hints in H3);
  185.               autorewrite with Hints;
  186.               try (rewrite (IH1 (a :: l2) b Heqb1) by (autorewrite with Hints; tauto));
  187.               try (rewrite (IH2 (a :: l2) b Heqb1) by (autorewrite with Hints; tauto));
  188.               try (rewrite <- USIJ; rewrite (IH3 (a :: l2) b Heqb1) by (autorewrite with Hints; tauto));
  189.               try (rewrite (IH4 (a :: l2) b Heqb1) by (autorewrite with Hints; tauto));
  190.               try (rewrite (IH1 l2 a H1 H2));
  191.               try (rewrite (IH2 l2 a H1 H2));
  192.               try (rewrite <- USIJ; rewrite (IH3 l2 a H1 H2));
  193.               try (rewrite (IH4 l2 a H1 H2));
  194.               try (rewrite H3);
  195.               try (rewrite (IH1 l2 b Heqb1 Heqb2));
  196.               try (rewrite (IH2 l2 b Heqb1 Heqb2));
  197.               try (rewrite <- USIJ; rewrite (IH3 l2 b Heqb1 Heqb2));
  198.               try (rewrite (IH4 l2 b Heqb1 Heqb2));
  199.               try tauto.
  200. Qed.
  201.  
  202. Lemma diff_simpl_1 : forall l1 l2 a, inbool a l1 = false -> inbool a l2 = false -> diff (a :: l2) l1 = diff l2 l1.
  203. Proof.
  204. intros l1.
  205. assert (H1 := diff_simpl l1).
  206. destruct H1 as [[H1 H2] [H3 H4]].
  207. tauto.
  208. Qed.
  209.  
  210. Lemma diff_simpl_2 : forall l1 l2 a, inbool a l1 = false -> inbool a l2 = true -> diff (a :: l2) l1 = diff l2 l1.
  211. Proof.
  212. intros l1.
  213. assert (H1 := diff_simpl l1).
  214. destruct H1 as [[H1 H2] [H3 H4]].
  215. tauto.
  216. Qed.
  217.  
  218. Lemma diff_simpl_3 : forall l1 l2 a, inbool a l1 = true -> inbool a l2 = false -> S (diff (a :: l2) l1) = diff l2 l1.
  219. Proof.
  220. intros l1.
  221. assert (H1 := diff_simpl l1).
  222. destruct H1 as [[H1 H2] [H3 H4]].
  223. tauto.
  224. Qed.
  225.  
  226. Lemma diff_simpl_4 : forall l1 l2 a, inbool a l1 = true -> inbool a l2 = true -> diff (a :: l2) l1 = diff l2 l1.
  227. Proof.
  228. intros l1.
  229. assert (H1 := diff_simpl l1).
  230. destruct H1 as [[H1 H2] [H3 H4]].
  231. tauto.
  232. Qed.
  233.  
  234. Hint Rewrite diff_simpl_1 diff_simpl_2 diff_simpl_3 diff_simpl_4 using autorewrite with Hints; tauto : Hints.
  235.  
  236. Lemma diff_le_length_le1:
  237.   forall l1 l2 a, diff (a::l2) l1 <= diff l2 l1.
  238. Proof.
  239. intros l1 l2 a;
  240.   try (
  241.       remember (inbool a l1) as b1;
  242.       symmetry in Heqb1;
  243.       destruct b1);
  244.     try (
  245.         remember (inbool a l2) as b2;
  246.         symmetry in Heqb2;
  247.         destruct b2);
  248.       rewrite <- HYAZ;
  249.       autorewrite with Hints;
  250.       try tauto.
  251. Qed.

Update the Post

Either update this post and resubmit it with changes, or make a new post.

You may also comment on this post.

update paste below
details of the post (optional)

Note: Only the paste content is required, though the following information can be useful to others.

Save name / title?

(space separated, optional)



Please note that information posted here will expire by default in one month. If you do not want it to expire, please set the expiry time above. If it is set to expire, web search engines will not be allowed to index it prior to it expiring. Items that are not marked to expire will be indexable by search engines. Be careful with your passwords. All illegal activities will be reported and any information will be handed over to the authorities, so be good.

comments powered by Disqus
worth-right
worth-right
worth-right