V7.0 about coq

[coqbot]

Bonjour,

Voila qq bugs rencontres lors de mes premiers essais avec la V7.

Installation de coq-7.0-1.i386.rpm sur une redhat 6.1 sur un i586.

Bugs :

1. J'ai du installe le package rpm avec l'option "-ignorearch", car sinon
   j'avais le message d'erreur
   "package coq-7.0-1 is for a different architecture"

2. Le script "translate_V6-3-1_to_V7-0" me rajoute des points d'interrogation
   partout dans mes fichiers, mais je ne comprends pas trop pourquoi (un bug de
   sed 3.02 ???). Apres la modif suivante, ca a l'air de marcher:
   11c11
   < -e "s/</ </g" -e "s/|</| </g" -e "s/([^ ])?/\1 ?/g" \

---

-e "s/~</~ </g" -e "s/|</| </g" -e "s/\?/ \?/g" -e "s/  / /g" \

3. La compilation du fichier coq joint ci-dessous termine sur l'erreur

In environment
A : Set
c : clock
F0 : (samplStr c)->(samplStr c)
rec0_tmp : (n:nat)(samplStr c)->(samplStr (clock_nth_tl n c))
n : nat
s : (samplStr c)
x := (F0 s) : (samplStr c)
The term (sp_cons (sp_nth n x) (rec0_tmp (S n) x)) has type
(samplStr (clock_nth_tl n c)) while it is expected to have type
(samplStr (clock_nth_tl s c))

Le type attendu n'a pas de sens, alors que le type trouve en a un !

(Ce fichier est accepte en V6.3.1 et V6.2.2, modulo le changement de syntaxe,
ie ici "Implicit Arguments On.")

Cordialement,

Sylvain.

---

Set Implicit Arguments.

Require Export Streams.
Require Export Bool.

Section Sampled_streams.

Definition clock:=(Stream bool).
(* Clocks are Streams of booleans )
( "true" corresponds to a "tic" )
( "false" corresponds to a delay *)

Variable A : Set. (* the set of elt in sampled streams *)

(* A sampled stream is a "stream" of "samplSets" *)

Inductive samplSet: bool -> Set :=
None: (samplSet false)
| Any: A -> (samplSet true)
| Fail: (samplSet true) (* initialization error *).

(* Set of sampled Streams *)
CoInductive samplStr: clock -> Set :=
sp_cons: (c:clock)(samplSet (hd c))->(samplStr (tl c))->(samplStr c).

(* Generics destructors *)

Definition sp_hd :=
[c:clock; x: (samplStr c)]
<c:clock; x: (samplStr c)>
Cases x of (sp_cons _ a _) => a end.

Definition sp_tl :=
[c:clock; x: (samplStr c)]
<c:clock; x: (samplStr c)>
Cases x of (sp_cons _ _ s) => s end.

Fixpoint clock_nth_tl [n:nat] : clock->clock :=
[c:clock] Cases n of
O => c
|(S m) => (tl (clock_nth_tl m c))
end.

Definition clock_nth : nat->clock->bool :=
[n:nat]s:clock.

(* nth power of sp_tl for samplStrs *)
Fixpoint sp_nth_tl [n:nat] :
(c:clock)(samplStr c)->(samplStr (clock_nth_tl n c)) :=
[c:clock; s:(samplStr c)]
<n:nat>Cases n of
O => s
|(S m) => (sp_tl (sp_nth_tl m s))
end.

Definition sp_nth :
(n:nat; c:clock)(samplStr c)-> (samplSet (clock_nth n c)) :=
n;c;s.

Variable c: clock. (* we work at constant clock. *)

Variable F0: (samplStr c) -> (samplStr c).

CoFixpoint rec0_tmp: (n:nat)(samplStr c)
->(samplStr (clock_nth_tl n c)):=
[n; s]
let x=(F0 s) in (sp_cons (sp_nth n x) (rec0_tmp (S n) x)).

[coqbot]

Pb 2 and 3 are fixed.
1 is a problem related to the arch of the rpm different from the workstation's
arch
(i386/i586).
Obsolete (01/2003)