The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT cnam.fr>]

On Tue, 25 Jul 2006 15:49:59 -0500 "Andrew Gacek" 
<andrew.gacek AT gmail.com>
 wrote:
>  Inductive term : Set :=
>   | one : term
>   | app : term -> term -> term
>   | lam : term -> term
>   | clos : term -> env -> term
>   with env : Set :=
>   | id : env
>   | shift : env
>   | cons : term -> env -> env
>   | merge : env -> env -> env.
> 
>  Scheme term_env_ind := Induction for term Sort Prop
>   with env_term_ind := Induction for env Sort Prop.
> 
> Theorem Inverse : forall (t : Sigma.term) (e : Sigma.env),
>   susp_to_sigma_term (sigma_to_susp_term t) = t /\
>   susp_to_sigma_env (sigma_to_susp_env e) (sigma_to_susp_nl e) = e.
> 
> Have I stated the induction schemes correctly? 

yes

> Is the theorem in
> proper form to apply those schemes? If so, how?

No, you have to chose one of the two properties as "the one you prove"
and use the other as a parameter of the principle you will use (see the
type of term_env_ind : it takes two predicates as arguments BUT the
conclusion is about one of them). This should give you the idea:

Inductive term : Set :=
  | one : term
  | app : term -> term -> term
  | lam : term -> term
  | clos : term -> env -> term
  with env : Set :=
  | id : env
  | shift : env
  | cons : term -> env -> env
  | merge : env -> env -> env.

 Scheme term_env_ind := Induction for term Sort Prop
  with env_term_ind := Induction for env Sort Prop.

(* don't know all these*)
 Variable sigma : Set.
 Variable sigma_to_susp_term : term -> sigma.
 Variable sigma_to_susp_env : env -> sigma.
 Variable susp_to_sigma_term : sigma -> term.
 Variable susp_to_sigma_env : sigma -> sigma -> env.
 Variable sigma_to_susp_nl : env -> sigma.

Theorem Inverse : forall (t : term), susp_to_sigma_term (sigma_to_susp_term 
t) = t.
  intros t.

  induction t using term_env_ind 
    with (P0:=fun e:env => susp_to_sigma_env (sigma_to_susp_env e) 
(sigma_to_susp_nl e) = e).



> Thanks,
> Andrew Gacek