Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
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
You can’t perform that action at this time.