The Coq mailing list

[Pierre Geneves <pgeneves AT us.ibm.com>]

Here is a basic example of my question:

Inductive G : Set :=
  | a : G1 -> G -> G
  | b : G1 -> G

with G1 : Set :=
  | c : G1 -> G1 -> G1
  | d : nat -> nat -> G1.


Inductive Gp : Set :=
  | m : Gp -> Gp -> Gp ->
Gp
  | n : Gp -> Gp -> Gp
  | p : nat -> Gp
  | q : nat -> Gp.


Fixpoint D (t : G) : Gp:=
  match t with
  | a t1 t2 => match t1 with
          |
c u1 u2 => n (q 1) (D t2) 
          |
d n1 n2 => p n2
          end
  | b t1 => p 2
  end.



(* At this stage, I can involve G terms
in proofs, and make Coq compute their translation by D: *)

Goal (D(a (d 1 2) (b (d 2 3))))=(D (b
(d 1 2))).
Proof.
simpl; reflexivity.
Qed.



Now, what about computing automatically
the subset of Gp given by D? Or in other terms, can Coq compute the inductive
set that contains all and only all translations that D can output?

(for example, the construct "m"
of Gp is not used in D so "m" will never appear in a term outputted
by D; 
"q" only occurs as the first
subterm of the construct "n", ...)

Thanks,

Pierre

Pierre Geneves/Watson/IBM@IBMUS
Sent by: coq-club-admin AT pauillac.inria.fr

06/23/2004 04:55 PM

To	coq-club AT pauillac.inria.fr
cc
Subject	[Coq-Club] Computing restricted inductive sets

Hello, 

I have two different abstract syntaxes G and G', along with a derivor D
that maps each construct of G to a specific construct of G' using rewriting
rules. I am interested in identifying the abstract syntax of D(G), which
is a restriction of G'. Let's consider that both G and G' are first order
for now. 

I guess that Coq can automatically infer the output inductive type of D(G).
I am looking for a convenient way to trigger this computation and print
the output. 

I have naively started by encoding G as an inductive set definition. I
have then tried to encode D as a fixpoint that takes a term of G as a parameter
and outputs its translation by D. I have also tried to encode D as rewriting
rules for using the "AutoRewrite" tactic. My attempts so far
force me to encode G' (ok, but kind of overkill). They allow me to handle
instances of G, but I haven't found a way to automatically get D(G) yet.
I realize that the answer could be obvious (a simple lemma or definition?)
but I don't find it. Also, there might be better ways for encoding my problem...

Any hints, suggestions, or pointers? 

Thank you! 

Pierre