The Coq mailing list

[Takashi MIYAMOTO <tmiya AT bu.iij4u.or.jp>]

Dear Pierre, 

On 2012/01/07, at 19:11, Pierre Boutillier wrote:

> Hi,
> The advise is : { z | P z } is an inductive type, (exist _ z (_ : P Z)) is 
> the constructor of type {z | P z}
> 
> -8<------
> Definition ZHs_of_Zs(zs:list Z)(*H:forall z, In z zs -> (0<=z<Max)%Z*) 
> :list ZH.
> refine ((fix f (zs:list Z)(*_:f z, In z zs -> (0<=z<Max)%Z*):list ZH :=
> match zs return (list ZH) with
> | nil => nil
> | cons z zs' => cons (exist _ z  _) (f zs')
> end) zs).
> -8<------
> will be better :-)

Thank you for your advice. It makes one step forward, but still I cannot 
prove the function.

After use of refine tactic in the following proof, zs (or zs0) seems to be 
(cons z zs'),
however, there is no assumptions like H1:zs0 = cons z zs'. 
How can I have relations between zs, z, and zs' ?

Thank you in advance.

---

Coq < Require Import ZArith.
Coq < Require Import List.
Coq < Parameter Max:Z.
Coq < Parameter HMax:(Max >= 2)%Z.
Coq < Definition ZHs_of_Zs(zs:list Z)(H:forall z, In z zs -> 
(0<=z<Max)%Z):list {z:Z | (0<=z<Max)%Z}.
1 subgoal
  
  zs : list Z
  H : forall z : Z, In z zs -> (0 <= z < Max)%Z
  ============================
   list {z : Z | (0 <= z < Max)%Z}

ZHs_of_Zs < refine ((fix f (zs:list Z)(H:forall z, In z zs -> (0<=z<Max)%Z) :=
ZHs_of_Zs < match zs as zs0 return list {z:Z|(0<=z<Max)%Z} with
ZHs_of_Zs < | nil => nil
ZHs_of_Zs < | cons z zs' => cons (exist _ z _) (f zs' _)
ZHs_of_Zs < end) zs H).
2 subgoals
  
  zs : list Z
  H : forall z : Z, In z zs -> (0 <= z < Max)%Z
  f : forall zs : list Z,
      (forall z : Z, In z zs -> (0 <= z < Max)%Z) ->
      list {z : Z | (0 <= z < Max)%Z}
  zs0 : list Z
  H0 : forall z : Z, In z zs0 -> (0 <= z < Max)%Z
  z : Z
  zs' : list Z
  ============================
   (0 <= z < Max)%Z

subgoal 2 is:
 forall z0 : Z, In z0 zs' -> (0 <= z0 < Max)%Z

ZHs_of_Zs < 

===================================
Takashi Miyamoto
http://www.imasy.or.jp/~miyamoto/
http://tmiya.blogspot.com/