Create a gist now

Instantly share code, notes, and snippets.

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