The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Tom Prince wrote:
> Inductive Term :=
>    | Var: nat → Term
>    | Op: Term → Term → Term.
>
> Fixpoint eval_term {A: Type} (op: A → A → A) (var: nat → A) (t: Term) :=
>    match t with
>      | Var n =>  var n
>      | Op x y =>  op (eval_term op var x) (eval_term op var y)
>    end.
>
> Inductive Equal := Eq: Term → Term → Equal.
>
> Fixpoint eval_eq {A: Type} (op: A → A → A) (var: nat → A) (e: Equal) :=
>    let (x, y) := e in (eval_term op var x) = (eval_term op var y).
>
> Inductive Laws : Equal ->  Prop :=
>    | law_1 : Laws (Eq (Var 0) (Op (Var 0) (Var 1)))
>    | law_2 : Laws (Eq (Op (Var 0) (Var 0)) (Op (Var 1) (Var 0))).
>
> Axiom (A: Type).
> Axiom (op: A→A→A).
>
> Axiom (laws_true: ∀ {E} (_: Laws E), ∀ x y, eval_eq op (fun n =>  match n with | 0 
> =>  x | _ =>  y end) E).
>
> Record rec (A: Type) (op: A→A→A) := { m1 : ∀ x y, x = (op x y) ; m2: ∀ x y, 
> (op x x) = (op y x) }.
>
> Goal rec A op.
>    

The following doesn't strike me as so bad:

Hint Extern 1 => apply (laws_true law_1) || apply (laws_true law_2).
Hint Constructors rec.

Goal rec A op.
  auto.
Qed.