Advertisement
Guest User

Untitled

a guest
Apr 18th, 2015
187
0
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 0.98 KB | None | 0 0
  1. lolcathost% coqtop
  2. Welcome to Coq 8.4pl6 (April 2015)
  3.  
  4. Coq < Theorem plus_0_r : forall n, n + 0 = n.
  5. 1 subgoal
  6.  
  7. ============================
  8. forall n : nat, n + 0 = n
  9.  
  10. plus_0_r < induction n; firstorder.
  11. No more subgoals.
  12.  
  13. plus_0_r < Qed.
  14. induction n; firstorder .
  15.  
  16. plus_0_r is defined
  17.  
  18. Coq < Theorem plus_n_Sm : forall n m, S (n + m) = n + S m.
  19. 1 subgoal
  20.  
  21. ============================
  22. forall n m : nat, S (n + m) = n + S m
  23.  
  24. plus_n_Sm < induction n; firstorder.
  25. No more subgoals.
  26.  
  27. plus_n_Sm < Qed.
  28. induction n; firstorder .
  29.  
  30. plus_n_Sm is defined
  31.  
  32. Coq < Theorem plus_comm : forall n m, n + m = m + n.
  33. 1 subgoal
  34.  
  35. ============================
  36. forall n m : nat, n + m = m + n
  37.  
  38. plus_comm < induction m; first [ rewrite plus_0_r | rewrite <- plus_n_Sm; rewrite IHm ]; reflexivity.
  39. No more subgoals.
  40.  
  41. plus_comm < Qed.
  42. induction m; (first [ rewrite plus_0_r | rewrite <- plus_n_Sm; rewrite IHm ]);
  43. reflexivity.
  44.  
  45. plus_comm is defined
  46.  
  47. Coq <
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement