Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Equational Reasoning in Coq, using tactics inside terms!
Require Import Coq.Setoids.Setoid.
Require Import Arith.
Notation "`Begin p" := p (at level 20, right associativity).
Notation "a =] p ] pr" := (@eq_trans _ a _ _ p pr) (at level 30, right associativity).
Notation "a =[ p [ pr" := (@eq_trans _ a _ _ (eq_sym p) pr) (at level 30, right associativity).
Notation "a `End" := (@eq_refl _ a) (at level 10).
Definition times2 : forall n, n + n = 2 * n := fun n =>
`Begin
(n + n) =]$( rewrite (plus_n_O n) at 2; reflexivity )$]
(n + (n + 0)) =]$( reflexivity )$]
(2 * n)
`End.
Definition times2' : forall n, n + n = 2 * n := fun n =>
`Begin
(n + n) =]$( apply plus_n_O )$]
(n + n + 0) =[$( apply plus_assoc )$[
(n + (n + 0)) =]$( reflexivity )$]
(2 * n)
`End.
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.