The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi,

The statement of H refers to zs and, as Cedric showed, it needs to be
generalized over zs before matching. To do some advertising, in 8.4,
this can be done implicitly by adding a matching on H:

Require Import ZArith List.
Parameter Max:Z.
Parameter HMax:(Max >= 2)%Z.
Definition ZH := {z:Z | (0<=z<Max)%Z}.

Definition ZHs_of_Zs(zs:list Z)(H:forall z, In z zs -> (0<=z<Max)%Z) :list ZH.
refine ((fix f zs H : list ZH :=
  match zs, H with
  | nil, H => nil
  | z::zs', H => (exist _ z _) :: (f zs' _)
  end) zs H).
(* "Show Proof." shows the generalization *)
simpl In in *; auto.
simpl In in *; auto.
Defined.

Hugo Herbelin

On Sat, Jan 07, 2012 at 01:42:23PM +0100, AUGER Cédric wrote:
> Le Sat, 7 Jan 2012 12:29:59 +0100,
> Pierre Boutillier 
>Â <pierre.boutillier AT pps.jussieu.fr>
>  a écrit :
> 
> > 
> > Le 7 janv. 12 à 12:14, Takashi MIYAMOTO a écrit :
> > 
> > > 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' ?
> > You use the dark magie of the return clause (my coq does not find ln  
> > definition so this is not tested and there must be typo):
> 
> There is no "ln", just "In" and it is perfectly valid.
> I guess wether Pierre rewrote the code by hand (surprising), whether he
> forgot to import List (although this import was part of your sample).
> 
> > >> 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 as zs0 return (f z, In z zs0 -> (0<=z<Max)%Z*)) -> list
> > >> ZH with
> > >> | nil => fun H' => nil
> > >> | cons z zs' => fun H' => cons (exist _ z  _) (f zs')
> > >> end) zs H).
> > 
> > (the return clause should be in fact infered)
> > 
> > Pierre Boutillier
>Â >Â pierre.boutillier AT pps.jussieu.fr
> 
>  ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂
> Definition ν {A:Type} {P:A->Prop} (x:sig P) : A :=
>   match x with
>   | exist a _ => a
>   end.
> 
> Definition π {A:Type} {P:A->Prop} (x:sig P) : P (ν x) :=
>   match x with
>   | exist _ p => p
>   end.
> 
> Notation "'{:' x ':}'" := (exist _ x _).
> 
> (*Those two functions are here to make nicer terms by having direct
>   access to the witness and to the proof.
>   I sometimes redefine "sig" as:
>   Record spec {A:Type} (P:A->Prop) := { ν: A
>                                       ; π: P ν
>                                       }.
>   which is exactly "sig" modulo renaming (sig<->spec)
>   (exist<->Build_sig).
>   But this way it automatically generates "ν" and "π".
> 
>   The notation "{: x :}" is only to avoid these ugly "exist _ x _"
>   which makes them harder to read and have two different "_" one
>   is to be automatically infered by the type system, the other
>   will be one to fill by hand later.
> 
>   This notation is used on my tutorial on extraction you can
>   find on the Cocorico Wiki
> *)
> 
> Require Import ZArith.
> Require Import List.
> Parameter Max:Z.
> Parameter HMax:(Max >= 2)%Z.
> 
> Fixpoint ZHs_of_Zs zs: (forall z, In z zs -> (0<=z<Max)%Z) ->
>                        list {z:Z | (0<=z<Max)%Z}.
>  refine (match zs with
>          | nil => fun _ => nil
>          | cons z zs => fun H => cons {:z(*p1*):} (ZHs_of_Zs zs _(*p2*))
>          end).
>  (* Note that I put the hypothesis under the "match" so that the "zs"
>     contained in the hypothesis will also be destructured.
>     It would have been more work if I had written
>     "fun H => match zs ..." instead *)
> Proof. (*p1*)
>  clear - H. (* at least you have to remove ZHs_of_Zs if you want to use
>                the abstract tactic. If you don't want to use abstract
>                tactic, you don't have to bother of what you want to
>                clear. *)
>  abstract (exact (H z (or_introl _ (eq_refl _)))).
> Proof. (*p2*)
>  clear - H.
>  abstract (exact (fun z K => H z (or_intror _ K))).
> Defined.
> 
> Print ZHs_of_Zs.
> 
>  ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂
> I used the abstract and the exact tactics if you find them ugly/not
> convenient/hard to use/…, you can do:
> 
> Fixpoint ZHs_of_Zs zs: (forall z, In z zs -> (0<=z<Max)%Z) ->
>                        list {z:Z | (0<=z<Max)%Z}.
>  refine (match zs with
>          | nil => fun _ => nil
>          | cons z zs => fun H => cons {:z(*p1*):} (ZHs_of_Zs zs _(*p2*))
>          end).
> Proof. (*p1*)
>  firstorder.
> Proof. (*p2*)
>  firstorder.
> Defined.
> 
> For instance (Note also that none of the "Proof." are mandatory).
> But terms will be uglier (Print ZHs_of_Zs).
>