Quelle Case17.v Sprache: Coq

(* Check the synthesis of predicate from a cast in case of matching of
   the first component (here [list bool]) of a dependent type (here [sigT])
   (Simplification of an example from file parsing2.v of the Coq'Art
    exercises) *)

Parameter parse_rel : list bool -> list bool -> nat -> Prop.

Parameter (l0 : list bool)
  (rec :
     forall l' : list bool,
     length l' <= S (length l0) ->
     {l'' : list bool &
     {t : nat | parse_rel l' l'' t /\ length l'' <= length l'}} +
     {(forall (l'' : list bool) (t : nat), ~ parse_rel l' l'' t)}).

Axiom HHH : forall A : Prop, A.

Check
  (match rec l0 (HHH _) with
   | inleft (existT _ (cons false l1) _) => inright _ (HHH _)
   | inleft (existT _ (cons true l1) (exist _ t1 (conj Hp Hl))) =>
       inright _ (HHH _)
   | inleft (existT _ _ _) => inright _ (HHH _)
   | inright Hnp => inright _ (HHH _)
   end
   :{l'' : list bool &
    {t : nat | parse_rel (true :: l0) l'' t /\ length l'' <= S (length l0)}} +
    {(forall (l'' : list bool) (t : nat), ~ parse_rel (true :: l0) l'' t)}).

(* The same but with relative links to l0 and rec *)

Check
  (fun (l0 : list bool)
     (rec : forall l' : list bool,
            length l' <= S (length l0) ->
            {l'' : list bool &
            {t : nat | parse_rel l' l'' t /\ length l'' <= length l'}} +
            {(forall (l'' : list bool) (t : nat), ~ parse_rel l' l'' t)}) =>
   match rec l0 (HHH _) with
   | inleft (existT _ (cons false l1) _) => inright _ (HHH _)
   | inleft (existT _ (cons true l1) (exist _ t1 (conj Hp Hl))) =>
       inright _ (HHH _)
   | inleft (existT _ _ _) => inright _ (HHH _)
   | inright Hnp => inright _ (HHH _)
   end
   :{l'' : list bool &
    {t : nat | parse_rel (true :: l0) l'' t /\ length l'' <= S (length l0)}} +
    {(forall (l'' : list bool) (t : nat), ~ parse_rel (true :: l0) l'' t)}).

quality98%

¤ Dauer der Verarbeitung: 0.2 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.