coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: muad <muad.dib.space AT gmail.com>
- To: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] Simple example
- Date: Thu, 19 Feb 2009 12:43:10 -0800 (PST)
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Require Import List.
(* To adapt your specification a bit it makes sense to use
* 'sumbool' from Coq standard library:
*)
Definition Decide (P : Prop) := { P } + { ~ P }.
(* P is a Proposition, so it will be erased on extraction,
* the remaining information (in ocaml) will simple be
* which branch (i.e. if P was contructed or shown
* contradictory)
*)
Section Sublist.
Variable A : Type.
(* The program(s) are parametrized over some type of elements *)
Variable eq_A_dec : forall x y : A, Decide (x = y).
(* And we have to be able to see if they are equal or not *)
Section Specification.
(* what does it mean to be a sublist? *)
Definition Sublist (sub list : list A) :=
exists begin, exists tail, begin ++ sub ++ tail = list.
(* The type of programs which decide if one list is a
* sublist of another:
*)
Definition Sublist_spec (sub list : list A) :=
Decide (Sublist sub list).
End Specification.
(* Now we can attempt to realize the specification by giving an
* implementation inside Coq with this type
*)
Section Implementation.
Section Subproblem.
(* As usual in programming (and proofs), diving into subproblems
* will make things much easier:
*)
Definition Prefix (pre list : list A) :=
exists tail, pre ++ tail = list.
Definition Prefix_spec (pre list : list A) :=
Decide (Prefix pre list).
Definition Prefix_dec (pre list : list A) : Prefix_spec pre list.
refine (
fix Prefix_dec (pre list : list A) : Prefix_spec pre list := _
).
refine (
match pre as pre return Prefix_spec pre list with
| nil => left _ _
| p :: ps => _
end
).
unfold Prefix.
exists list.
reflexivity.
refine (
match list as list return Prefix_spec (p :: ps) list with
| nil => right _ _
| x :: xs => _
end
).
intros [x H].
simpl in H.
discriminate H.
refine (
match eq_A_dec p x with
| left eqPrf => (* the first two elements of both lists are equal
*)
match Prefix_dec ps xs with
| left prePrf => left _ _
| right nprePrf => right _ _
end
| right nqPrf => (* they are not equal *)
right _ _
end
).
subst.
destruct prePrf as [tail tailPrf].
exists tail; rewrite <- tailPrf.
reflexivity.
subst.
intros [tail tailPrf]; apply nprePrf.
exists tail; injection tailPrf; congruence.
intros [tail tailPrf]; apply nqPrf.
injection tailPrf; congruence.
Defined.
End Subproblem.
(* and then define the Sublist function in a similar way .. *)
End Implementation.
End Sublist.
Extraction Prefix_dec.
And then extraction gives:
(** val prefix_dec :
('a1 -> 'a1 -> decide) -> 'a1 list -> 'a1 list -> 'a1 prefix_spec **)
let rec prefix_dec eq_A_dec pre list0 =
match pre with
| Nil -> Left
| Cons (p, ps) ->
(match list0 with
| Nil -> Right
| Cons (x, xs) ->
(match eq_A_dec p x with
| Left -> prefix_dec eq_A_dec ps xs
| Right -> Right))
--
View this message in context:
http://www.nabble.com/Simple-example-tp22106715p22109277.html
Sent from the Coq mailing list archive at Nabble.com.
- [Coq-Club] Simple example, silviu andrica
- Re: [Coq-Club] Simple example,
Adam Chlipala
- Re: [Coq-Club] Simple example,
silviu andrica
- Re: [Coq-Club] Simple example,
Cedric Auger
- Re: [Coq-Club] Simple example, Adam Chlipala
- Re: [Coq-Club] Simple example,
Cedric Auger
- Re: [Coq-Club] Simple example,
silviu andrica
- Re: [Coq-Club] Simple example, muad
- Re: [Coq-Club] Simple example,
Adam Chlipala
Archive powered by MhonArc 2.6.16.