Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- lolcathost% coqtop
- Welcome to Coq 8.4pl6 (April 2015)
- Coq < Theorem plus_0_r : forall n, n + 0 = n.
- 1 subgoal
- ============================
- forall n : nat, n + 0 = n
- plus_0_r < induction n; firstorder.
- No more subgoals.
- plus_0_r < Qed.
- induction n; firstorder .
- plus_0_r is defined
- Coq < Theorem plus_n_Sm : forall n m, S (n + m) = n + S m.
- 1 subgoal
- ============================
- forall n m : nat, S (n + m) = n + S m
- plus_n_Sm < induction n; firstorder.
- No more subgoals.
- plus_n_Sm < Qed.
- induction n; firstorder .
- plus_n_Sm is defined
- Coq < Theorem plus_comm : forall n m, n + m = m + n.
- 1 subgoal
- ============================
- forall n m : nat, n + m = m + n
- plus_comm < induction m; first [ rewrite plus_0_r | rewrite <- plus_n_Sm; rewrite IHm ]; reflexivity.
- No more subgoals.
- plus_comm < Qed.
- induction m; (first [ rewrite plus_0_r | rewrite <- plus_n_Sm; rewrite IHm ]);
- reflexivity.
- plus_comm is defined
- Coq <
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement