The Coq mailing list

[Fr�d�ric Gava <gava AT univ-paris12.fr>]

Dear Coq-club,

It is a little problem, perhaps just missing the good tactic...

I have a problem for proving that an inductive is exclusive to a 
co-inductive (for semantics) as in :
http://pauillac.inria.fr/~xleroy/coindsem/doc/semantics.html

here the code (I have omit details and write axioms for what I have 
proved before). I write "co_" for the co_inductive. My (co)-inductives 
of evaluation (noted eval_glo) used (co)-inductives for evaluation of 
sub-part of the language. Noted that my problem cames from "forall i:Z" 
and "exists n:Z" but I need them.

Many thanks,
Frédéric Gava

Require Export ZArith.
Open Scope Z_scope.

Parameter env:Set.
Parameter instr:Set.

(* a co-inductive for co-evaluation *)
Parameter co_eval_loc:Z-> env -> instr -> Prop.

(* an inductive that is deterministic and exclusive to the co-inductive 
one *)
Parameter eval_loc:Z-> env -> instr -> env-> Prop.

(* exclusive *)
Axiom eval_loc_and_co_eval_loc_exclusive: forall i envB instr envR,
 eval_loc i envB instr envR -> co_eval_loc i envB instr -> False.

(* deterministic *)
Axiom eval_loc_determinist: forall i envB instr envR,
 eval_loc i envB instr envR -> forall envR', eval_loc i envB instr 
envR' -> envR'=envR.

Parameter p:Z.
Axiom positive_p: p>0.

(* this "function" is not really important and can be omitted *)
Parameter trans:(Z->env)->(Z->env)->Prop.

(* the transition is deterministic *)
Axiom trans_determinist: forall envB envR,
  trans envB envR -> forall envR', trans envB envR -> envR'=envR.


(* Here my inductive *)

Inductive eval_glo: (Z -> env) -> (Z -> instr) -> (Z -> env) -> Prop :=
 | eval_glo_all : forall e i e',
    (forall n, (0<=n<p) -> (eval_loc n (e n) (i n) (e' n)))
    -> eval_glo e i e'

 | eval_glo_trans : forall e i e' ec e'' c,
    (forall n, (0<=n<p) -> (eval_loc n (e n) (i n) (e' n))) ->
    trans e' ec ->
    eval_glo ec c e'' ->
    eval_glo e i e''.


(* here my co-inductive *)

CoInductive co_eval_glo : (Z -> env) -> (Z -> instr) -> Prop :=
 | co_eval_glo_trans: forall e i e' ec,
    (forall n, (0<=n<p) -> (eval_loc n (e n) (i n) (e' n))) ->
    trans e' ec ->
    co_eval_glo ec i ->
    co_eval_glo e i

| co_eval_glo_exists: forall e i,
    (exists n, (0<=n<p) -> (co_eval_loc n (e n) (i n)))
    -> co_eval_glo e i.


Axiom i_dont_know_how_to_do_so_i_cheat: False.

(* The lemma that I can not prove it *)
Lemma eval_glo_and_co_eval_glo_exclusive: forall envB instr envR,
 eval_glo envB instr envR -> co_eval_glo envB instr -> False.

 induction 1;intros.

 inversion H0;intros.
 subst.
 (* Here I would like to have (e'0 n)=(e' n) forall n using 
eval_loc_determinist *)
 apply i_dont_know_how_to_do_so_i_cheat.

 subst.
 elim H1;intros.
 (* Here I have x:Z but not 0<=x<p  and I can't use 
eval_loc_and_co_eval_loc_exclusive *)
 apply i_dont_know_how_to_do_so_i_cheat.

 etc.