Equational Reasoning in Coq using Tactic Notations
Tactic Notation | |
"`Begin " constr(lhs) := idtac. | |
Tactic Notation | |
"≡⟨ " tactic(proof) "⟩" constr(lhs) := | |
(stepl lhs by proof). | |
Tactic Notation | |
"≡⟨ " tactic(proof) "⟩" constr(lhs) "`End" := | |
(now stepl lhs by proof). | |
Require Import Coq.Init.Peano. | |
Theorem plus_comm : | |
forall (m n : nat), m + n = n + m. | |
Proof. | |
intros m n. | |
induction n. | |
- `Begin | |
(m + 0). | |
≡⟨ now rewrite <- plus_n_O ⟩ | |
(m). | |
≡⟨ reflexivity ⟩ | |
(0 + m) | |
`End. | |
- `Begin | |
(m + S n). | |
≡⟨ now rewrite plus_n_Sm ⟩ | |
(S (m + n)). | |
≡⟨ now rewrite IHn ⟩ | |
(S (n + m)). | |
≡⟨ reflexivity ⟩ | |
(S n + m) | |
`End. | |
Qed. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment