The Coq mailing list

[Castéran Pierre <pierre.casteran AT gmail.com>]

Hello,

  You can define isPrefixOf as an inductive predicate :

Inductive isPrefixOf {A:Type}: relation (list A) :=

  pf1 : forall x,  isPrefixOf nil x

| pf2 : forall a x y, isPrefixOf x y -> isPrefixOf (a::x) (a::y).

Then prove a small inversion lemma:

Lemma isPrefix_inv {A:Type} (x y: list A) (a b:A) :

  isPrefixOf (a::x) (b::y) -> a = b /\ isPrefixOf x y.

Proof. inversion 1; auto. Qed.

Then you prove an equivalence between this definition and your sig definition (by induction on the lists, and applications of IsPrefix_inv).

Lemma isPrefixOf_ok {A} (x y:list A) : isPrefixOf x y -> {z | x ++ z = y}.

Lemma isPrefixOf_okR {A} (x y z:list A) : x ++ z = y ->  isPrefixOf x y.

Best regards,

Pierre

Le 10 août 2020 à 05:55, Agnishom Chattopadhyay <agnishom AT cmi.ac.in> a écrit :

I have a function that is something like this:

 Definition isPrefixOf (x : list A) (y : list A) :=
     exists z, x ++ z = y.

Now, I want to define a witness function. Informally, it can be described as follows: Given x and y such that (isPrefixOf x y), return z which satisfies the criteria exists z, x ++ z = y.

I would try to define it this way, but that would not work (possibly because exists z, x ++ z = y is a Prop and we are asking for something in Type) :

Definition witness (x y : list A) {H : isPrefixOf x y} : list A.
    destruct H.

Abort.

Another option seems to be to define

Definition isPrefixOf (x y : list A) :=
    sig (fun z => x ++ z = y).

But I do not like this because this does not let me define things like Instance isPrefixOf_PreOrder : PreOrder isPrefixOf.

So, how can I have my cake and eat it too?