API tools faq
paste
Advertisement
Guest User

Untitled

a guest
Apr 28th, 2015
192
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 2.92 KB | None | 0 0
raw download clone embed print report
  1. Parameter A B C : Prop.
  2.  
  3. Lemma th1 : A -> B -> A.
  4. intros.
  5. apply (H).
  6. Save.
  7.  
  8. Lemma th2 : (A -> B -> C) -> (A -> B) -> A -> C.
  9. intros.
  10. apply(H).
  11. assumption.
  12. apply(H0 H1).
  13. Save.
  14.  
  15. Lemma th3 : A /\ B -> B.
  16. intros.
  17. elim H.
  18. intros.
  19. assumption.
  20. Save.
  21.  
  22. Lemma th4 : A -> B -> A/\B.
  23. intros.
  24. split.
  25. assumption.
  26. assumption.
  27. Save.
  28.  
  29. Lemma th5 : B -> A \/ B.
  30. intros.
  31. right.
  32. assumption.
  33. Save.
  34.  
  35. Lemma th6 : (A \/ B ) -> (A -> C) -> (B -> C) -> C.
  36. intros.
  37. elim H.
  38. assumption.
  39. assumption.
  40. Save.
  41.  
  42. Lemma th7 : A -> False -> ~A.
  43. intros.
  44. intro.
  45. assumption.
  46. Save.
  47.  
  48. Lemma th8 : False -> A.
  49. intro.
  50. elimtype False.
  51. assumption.
  52. Save.
  53.  
  54. Lemma th9 : (A <-> B) -> A -> B.
  55. intros.
  56. elim H.
  57. intros.
  58. apply(H1 H0).
  59. Save.
  60.  
  61. Lemma th10 : (A <-> B) -> B -> A.
  62. intros.
  63. elim H.
  64. intros.
  65. apply(H2 H0).
  66. Save.
  67.  
  68. Lemma th11 : (A -> B) -> (B -> A) -> (A <-> B).
  69. intros.
  70. split.
  71. assumption.
  72. assumption.
  73. Save.
  74.  
  75. Lemma th12 : (A -> B) -> (B -> A) -> (A <-> B).
  76. intros.
  77. tauto.
  78. Save.
  79.  
  80. Parameter E : Set.
  81. Parameter P : E -> Prop.
  82. Parameter Q : E -> E -> Prop.
  83.  
  84. Lemma th13 : ~(exists x : E, P x) -> forall x : E, ~P x.
  85. intros.
  86. intro.
  87. elim H.
  88. exists x.
  89. assumption.
  90. Save.
  91.  
  92. Lemma th14 : ( forall x : E, ~P x ) -> ~( exists x : E, P x ).
  93. intros.
  94. intro.
  95. elim H0.
  96. intros.
  97. apply(H x).
  98. assumption.
  99. Save.
  100.  
  101. Lemma th15 : (exists y : E, (forall x : E , (Q x y ))) -> forall x : E ,(exists y : E, (Q x y )).
  102. intros.
  103. elim H.
  104. intros.
  105. exists x0.
  106. apply(H0).
  107. Save.
  108.  
  109. Lemma th18 : (forall n : nat, (mult n 1) = n).
  110. intros.
  111. elim n.
  112. simpl.
  113. reflexivity.
  114. intros.
  115. simpl.
  116. rewrite H.
  117. reflexivity.
  118. Save.
  119.  
  120. Fixpoint f (n : nat) {struct n} : nat :=
  121. match n with
  122. | 0 => 1
  123. | S p => (mult 2 (f p))
  124. end.
  125. Lemma th19 : f(10) = 1024.
  126. intros.
  127. simpl.
  128. reflexivity.
  129. Save.
  130.  
  131. Open Scope list.
  132. Require Import List.
  133. Import ListNotations.
  134. Lemma th20 : (forall E:Type, (forall l : (list E), (forall e : E, rev (l ++ [e]) = e :: rev l))).
  135. intros.
  136. elim l.
  137. simpl.
  138. reflexivity.
  139. intros.
  140. simpl.
  141. rewrite H.
  142. reflexivity.
  143. Save.
  144.  
  145.  
  146. Lemma th21 : (forall E:Type, (forall l : (list E), rev (rev l) = l)).
  147. intros.
  148. elim l.
  149. simpl.
  150. reflexivity.
  151. intros.
  152. simpl.
  153. rewrite (th20 E0 (rev l0) a).
  154. rewrite H.
  155. simpl.
  156. reflexivity.
  157. Save.
  158.  
  159. Fixpoint fis_even (n : nat) {struct n} : Prop :=
  160. match n with
  161. | 0 => True
  162. | 1 => False
  163. | S (S p) => (fis_even p)
  164. end.
  165.  
  166. Inductive is_even : nat -> Prop :=
  167. | is_even_0 : is_even 0
  168. | is_even_S : forall n : nat, is_even n -> is_even (S (S n)).
  169.  
  170. Functional Scheme fis_even_ind := Induction for fis_even Sort Prop.
  171.  
  172. Lemma th22 : (forall n : nat,(fis_even n) -> (is_even n)).
  173. intro.
  174. functional induction (fis_even n).
  175. intro.
  176. apply is_even_0.
  177. intro.
  178. inversion H.
  179. intro.
  180. apply is_even_S.
  181. apply IHP0.
  182. apply H.
  183. Save.
  184.  
  185. Lemma th23 : (forall n : nat, (is_even n) -> (fis_even n)).
  186. intro.
  187. functional induction (fis_even n).
  188. intro.
  189. auto.
  190. intro.
  191. inversion H.
  192. intros.
  193. apply IHP0.
  194. inversion H.
  195. assumption.
  196. Save.
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement
Public Pastes
Advertisement
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
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!