The Coq mailing list

[Tom Prince <tom.prince AT ualberta.net>]

(*
On 2011-02-09, Adam Chlipala wrote:
> Tom Prince wrote:
> > Axiom param : nat ->  Type.
> > Axiom val : ∀ n, param n.
> >
> > [snip]
> >
> > Record rec := { m1 : param 0; m7: param 6; m6: param 5 }.
> >
> > Goal rec.
> >    
> 
> I think the example is abstracted a bit too much to illustrate the 
> issues, as [constructor; apply val] leads to the value of [rec] that 
> you're looking for.  Can you give a more complicated example which shows 
> what makes your real code trickier?

This is much closer to the actual code I am using. The actual code deals
with multiple operations of different arities. And there are at least
half a dozen different types coresponding to Laws and rec, with differnt
collection of operations/laws. (Hence my desire to automate the proof.

*)

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.
constructor.
let n:= fresh in (evar (n:Equal); assert (Laws n) as P; subst n; [ 
constructor 1 | apply (laws_true P)]).
let n:= fresh in (evar (n:Equal); assert (Laws n) as P; subst n; [ 
constructor 2 | apply (laws_true P)]).
Defined.

Goal rec A op.
Ltac TAC k := (let n:= fresh "n" in (evar (n:Equal); assert (Laws n) as P; 
subst n); [ constructor k | apply (laws_true P) ]).
constructor; [TAC 1 | TAC 2].