The Coq mailing list

[Frederic GAVA <frederic.gava AT wanadoo.fr>]

Bonjour,

J'ai ecris cette petite axiomatization (en changeant mon ancienne) mais j'ai 
maintenant
des problemes " Cannot solve a second-order unification problem" et puis plus 
tard des problemes
de conversion de termes.

Voici donc l'axiomatisation:

################################################################

Require Export ProgInt.

Require ZArith.
Require Bool.
Require Bool.Sumbool.
Require Omega.

(* ***** Parameters given by the BSMLlib library ***** *)

Parameters bsp_p:unit -> Z;
    Vector : Set -> Set;
    at: (T:Set) (Vector T) -> (i:Z) `0<=i<(bsp_p tt)` -> T;
    mkpar  : (T:Set) (Z -> T) -> (Vector T);
    apply  : (T1,T2:Set) (Vector (T1 -> T2)) 
                            -> (Vector T1) -> (Vector T2);
    put    : (T:Set)(Vector (Z -> (option T))) 
                                   -> (Vector (Z -> (option T)));
    ifat   : (T:Set) (Vector bool) -> Z -> T -> T -> T;
    super  : (T1,T2:Set) (unit -> (Vector T1)) 
      -> (unit -> (Vector T2))  -> ((Vector T1)*(Vector T2)).

(* ***** Axiom for the number of processes ***** *)
Axiom good_bsp_p:`0 < (bsp_p tt)`.


Definition within_bound: (i:Z) {`0<=i<(bsp_p tt)`}+{~`0<=i<(bsp_p tt)`}.
Intros; Case (Z_le_dec `0` i); Intros.
Intros; Case (Z_lt_dec i (bsp_p tt)); Intros; Auto.
Intuition.
Intuition.
Defined.

(* ***** Axiom of the asynchronous operators ***** *)
Axiom mkpar_def: (T:Set) (f:Z -> T)(i:Z) (H:`0 <= i < (bsp_p tt)`)
                    (at T (mkpar T f) i H)=(f i).
 
Axiom apply_def: (T1,T2:Set) (V1:(Vector (T1 -> T2))) 
                 (V2:(Vector T1 )) (i:Z) (H:`0 <= i < (bsp_p tt)`)
(at T2 (apply T1 T2 V1 V2) i H)=( (at (T1->T2) V1 i H) (at T1 V2 i H)).


(* **** Axiom of the communication-synchronisation operator *** *)
Axiom put_def: (T:Set)(Vf:(Vector (Z -> (option T)))) 
               (i:Z) (H:`0 <= i < (bsp_p tt)`)
((at (Z->(option T)) (put T Vf) i H)=([j:Z]
   if (within_bound j) then [H1]((at (Z-> (option T)) Vf j H1) i) 
                       else [H2](None T))).
    

(* ***** Axiom of the global synchronisation construction ***** *)
Axiom ifat_def: (T:Set)(V:(Vector bool)) (n:Z)(R_IF,R_ELSE:T)
(Hyp_n: `0 <= n < (bsp_p tt)`) ((ifat T V n R_IF R_ELSE)= 
        (if (sumbool_of_bool (at bool V n Hyp_n)) then [H1] R_IF 
           else [H2] R_ELSE)).
           
(* ***** Axiom for the parallel superposition ***** *)
Axiom super_def: (T1,T2:Set) (v1: unit -> (Vector T1)) 
  (v2: unit -> (Vector T2)) (super T1 T2 v1 v2)=((v1 tt),(v2 tt)).      

Hints Resolve good_bsp_p mkpar_def apply_def put_def super_def: datatypes 
v73. 


########################################################################

Ce que j'ai actuellement modifier et le fait que pour "at", il faille une 
preuve
que l'entier soit compris entre `0<=i<(bsp_p tt)` (ce qui peut paraitre 
normal).

Mais cette ajout me pose maintenant des probl&#65533;mes inatendus...

Voici donc le developpment d'un programme:


#######################################################################

(* des trivialite *)
Lemma egal_some: (T:Set)(a,b:T) ((Some ? a)=(Some ? b)) -> (a=b).
Intros.
Inversion H;Auto.
Qed.

Lemma some_egal:(T:Set)(a,b:T) (a=b) -> ((Some ? a)=(Some ? b)).
Intros.
Induction H;Auto.
Qed.

Lemma egal_reflexive: (T:Set)(a,b:T) (a=b)->(b=a).
Intros.
Rewrite H;Auto.
Qed.


(* Petite expression qui me sert souvent *)
Definition replicate : (T:Set)(a:T) {res: (Vector T) | (i:Z) (Hyp_i:`0 <=i < 
(bsp_p tt)`) (at T res i Hyp_i)=a}.
Intros.
Exists (mkpar T ([pid:Z]a)).
Intros.
Rewrite mkpar_def;Auto.
Defined.

(* Idem *)
Definition parfun : (T1,T2:Set)(f:T1->T2)(v:(Vector T1)) {res: (Vector T2) | 
(i:Z) (Hyp_i:`0 <=i < (bsp_p tt)`) (at T2 res i Hyp_i)= (f (at T1 v i 
Hyp_i))}.
Intros.
Refine Cases (replicate ? f) of
  (exist p h) => (exist ? ? (apply ? ? p v) ?) end.

Intros.
Rewrite apply_def;Auto.
Rewrite (h i Hyp_i);Trivial.
Defined.
##############################################################################



Et donc le programme principal:

#############################################################################
Definition  bcast_direct_tmp: (T:Set)(root:Z) (Hyp_root:`0<= root < (bsp_p 
tt)`) (vv:(Vector T))
  {res:(Vector (option T)) | (i:Z) (Hyp_i:`0 <=i < (bsp_p tt)`) ((at (option 
T) res i Hyp_i)=(Some T (at T vv root Hyp_root))) }.
Intros.
Refine let tosend=(mkpar (T->Z->(option T)) ([pid:Z][v:T] if (Z_eq_dec pid 
root) then [H1] ([dst:Z](Some T v)) 
                                                            else 
[H2]([dst:Z](None T)) ))
        in let recv=(put T (apply T (Z->(option T)) tosend vv))
        in Cases (replicate Z root) of
          (exist p h') => (exist ? ? (apply Z (option T) recv p) ?)
              end.
Intros.
Rewrite apply_def; Auto.
Unfold recv.
Rewrite put_def;Auto.
Case (within_bound (at Z p i Hyp_i));Intros;Auto.
Rewrite apply_def;Auto.
Unfold tosend.
Rewrite mkpar_def;Auto.
Case (Z_eq_dec (at Z p i Hyp_i) root) ;Intros.
??????????????????????????

################################################################################

Nous avons donc en resumer:
  root : Z
  Hyp_root : `0 <= root < (bsp_p tt)`
  vv : (Vector T)
  p : (Vector Z)
  i : Z
  Hyp_i : `0 <= i < (bsp_p tt)`
  a : `0 <= (at Z p i Hyp_i) < (bsp_p tt)`
  e : `(at Z p i Hyp_i) = root`
  ============================
   (Some T (at T vv (at Z p i Hyp_i) a))
    =(Some T (at T vv root Hyp_root))



Donc avant, je faisait "Rewrite e;Auto" et j'avais finis.


Mais maintenant j'ai:
Rewrite e.
Error: Cannot solve a second-order unification problem

Pourquoi ? 
Est-ce le fait que "a" soit une preuve pour "(at Z p i Hyp_i)" et pas pour 
"root" ?


Pour ne plus avoir ce probleme, je fais donc:

Generalize (egal_reflexive ? ? ? e);Intros.
NewInduction H.

et j'obtient:
  T : Set
  root : Z
  Hyp_root : `0 <= root < (bsp_p tt)`
  vv : (Vector T)
  p : (Vector Z)
  h' : (i:Z; Hyp_i:`0 <= i < (bsp_p tt)`)`(at Z p i Hyp_i) = root`
  i : Z
  Hyp_i : `0 <= i < (bsp_p tt)`
  a : `0 <= root < (bsp_p tt)`
  e : `root = root`
  ============================
   (Some T (at T vv root a))=(Some T (at T vv root Hyp_root))



Or "a" et "Hyp_root" sont de meme types et peuvent donc servir pour les meme 
choses.

Comment maintenant prouver cette egalite ?????
Est-ce possible ?
Peut on remplacer "Hyp_root" partout par "a" ?


Merci.

Frederic Gava