The Coq mailing list

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

On 2011-02-10, Adam Chlipala wrote:
> 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.
> 


That certainly works. I was hoping to avoid having to mention the names
of all the constructors twice. If I am going to have to mention them
twice anyway, I might as well just apply them by hand.

Right now, there are 6 files with this pattern in them, and there will
likely be more. Right now, they are mostly copy-pasted one from the
other, with just changes to the lists of laws, operations, and names of
records. (This is work extending Eelis' math-classes from
(https://github.com/eelis/math-classes) in particular, the files
src/varieties/{semigroup,semiring,ring}.v which I have so far extended
with monoid, group, and abgroup). 

I wonder if I should just learn to write tactics in ML. It seems as
though, while ltac is quite a rich language, it has quite a few gotchas
and awkward limitations. Now, I understand how this happend, but I
wonder if it would make to extend it with some more traditional
constructs, and the ability to do rich introspection.

  Tom