The Coq mailing list

["Cuihtlauac ALVARADO - STAGIAIRE A FT.BD/CNET/DTL/MSV" <Cuihtlauac.Alvarado AT cnet.francetelecom.fr>]

Hi,

I'm working on reflection too. I have an --- experimental --- tactic which 
might
be used as first step towards what you are aiming. Here comes an example :

(* Field.v *)

Require ListT.
Require Reify.

(* Target theory: Fields --------------------------------------------------- 
*)

Parameter A : Type.  
Parameter A_Null, A_Unit : A.
Parameter A_Opp, A_Inv : A -> A.
Parameter A_Plus, A_Mult : A -> A -> A.

Parameter A_Plus_commut : (x,y:A)(A_Plus x y)==(A_Plus y x).
Parameter A_Plus_assoc : (x,y,z:A)(A_Plus x (A_Plus y z))==(A_Plus (A_Plus x 
y)
z).
Parameter A_Plus_neutral_r : (x:A)(A_Plus x A_Null)==x.
Parameter A_Plus_invert_r : (x:A)(A_Plus x (A_Opp x))==A_Null.

Parameter A_Mult_assoc : (x,y,z:A)(A_Mult x (A_Mult y z))==(A_Mult (A_Mult x 
y)
z).
Parameter A_Mult_neutral_r : (x:A)(A_Mult x A_Unit)==x.
Parameter A_Mult_invert_r : (x:A)~(x==A_Null)->(A_Mult x (A_Inv x))==A_Unit.

Parameter A_distrib_l : (x,y,z:A)(A_Plus x (A_Mult y z))==(A_Mult (A_Plus x y)
(A_Plus x z)).
Parameter A_distrib_r : (x,y,z:A)(A_Plus (A_Mult x y) z)==(A_Mult (A_Plus x z)
(A_Plus y z)).

(* Reification stuff ------------------------------------------------------- 
*)

Parameter A_default : A.

Inductive fld : Set :=
  | f_Var : nat -> fld
  | f_Unit : fld
  | f_Null : fld
  | f_Inv : fld -> fld
  | f_Opp : fld -> fld
  | f_Mult : fld -> fld -> fld
  | f_Plus : fld -> fld -> fld.

Section Eval.

  Variable rho : (listT A). (* valuation *)

  Fixpoint f_eval [g:fld] : A :=
    Cases g of
      | (f_Var x) => (nth A A_default rho x)
      | f_Unit => A_Unit
      | f_Null => A_Null
      | (f_Inv g) => (A_Inv (f_eval g))
      | (f_Opp g) => (A_Opp (f_eval g))
      | (f_Mult f g) => (A_Mult (f_eval f) (f_eval g))
      | (f_Plus f g) => (A_Plus (f_eval f) (f_eval g))
    end.

End Eval.

With this stuff I can make a Coq session like that :

Coq < Load Field.

Blah, blah, blah...

Coq < Goal (x,y:A)(A_Opp (A_Plus x y))==(A_Plus (A_Opp y) (A_Opp x)).
1 subgoal
  
  ============================
   (x,y:A)(A_Opp (A_Plus x y))==(A_Plus (A_Opp y) (A_Opp x))

Unnamed_thm < Intros; Reify fld f_eval A A_default A_Unit A_Null A_Inv A_Opp
A_Mult A_Plus. Intros; Reify fld f_eval A A_default A_Unit A_Null A_Inv A_Opp
A_Mult A_Plus.
1 subgoal
  
  x : A
  y : A
  ============================
   (f_eval (cons A y (cons A x (nil A)))
     (f_Opp (f_Plus (f_Var (S O)) (f_Var O))))
    ==(f_eval (cons A y (cons A x (nil A)))
        (f_Plus (f_Opp (f_Var O)) (f_Opp (f_Var (S O)))))

Unnamed_thm < 

Here I get a goal with "field objects" which I might use the way I want. I'm
currently working on tools to automate & combine manipulations on those terms.

As you can see it's still very experimental since "Reify" should guess the 
right
inductive data structure encoding "target" field terms and the associate
evaluation function.

A work in progress...

-- 
Cuihtlauac ALVARADO
France Telecom - Branche Developpement - Cnet - DTL/MSV/MFL
Bureau WF 907 - 2, avenue Pierre Marzin - 22307 Lannion Cedex - France
Tel: {+33|0} 2 96 05 32 73 - Mobile: {+33|0} 6 08 10 80 41
Fax: {+33|0} 2 96 05 39 45