From 6b649aba925b6f7462da07599fe67ebb12a3460e Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Wed, 28 Jul 2004 21:54:47 +0000 Subject: Imported Upstream version 8.0pl1 --- test-suite/success/Case17.v | 45 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 45 insertions(+) create mode 100644 test-suite/success/Case17.v (limited to 'test-suite/success/Case17.v') diff --git a/test-suite/success/Case17.v b/test-suite/success/Case17.v new file mode 100644 index 00000000..07d64958 --- /dev/null +++ b/test-suite/success/Case17.v @@ -0,0 +1,45 @@ +(* Check the synthesis of predicate from a cast in case of matching of + the first component (here [list bool]) of a dependent type (here [sigS]) + (Simplification of an example from file parsing2.v of the Coq'Art + exercises) *) + +Require Import PolyList. + +Variable parse_rel : (list bool) -> (list bool) -> nat -> Prop. + +Variables l0:(list bool); rec:(l' : (list bool)) + (le (length l') (S (length l0))) -> + {l'' : (list bool) & + {t : nat | (parse_rel l' l'' t) /\ (le (length l'') (length l'))}} + + {(l'' : (list bool))(t : nat)~ (parse_rel l' l'' t)}. + +Axiom HHH : (A:Prop)A. + +Check (Cases (rec l0 (HHH ?)) of + | (inleft (existS (cons false l1) _)) => (inright ? ? (HHH ?)) + | (inleft (existS (cons true l1) (exist t1 (conj Hp Hl)))) => + (inright ? ? (HHH ?)) + | (inleft (existS _ _)) => (inright ? ? (HHH ?)) + | (inright Hnp) => (inright ? ? (HHH ?)) + end :: + {l'' : (list bool) & + {t : nat | (parse_rel (cons true l0) l'' t) /\ (le (length l'') (S (length l0)))}} + + {(l'' : (list bool)) (t : nat) ~ (parse_rel (cons true l0) l'' t)}). + +(* The same but with relative links to l0 and rec *) + +Check [l0:(list bool);rec:(l' : (list bool)) + (le (length l') (S (length l0))) -> + {l'' : (list bool) & + {t : nat | (parse_rel l' l'' t) /\ (le (length l'') (length l'))}} + + {(l'' : (list bool)) (t : nat) ~ (parse_rel l' l'' t)}] + (Cases (rec l0 (HHH ?)) of + | (inleft (existS (cons false l1) _)) => (inright ? ? (HHH ?)) + | (inleft (existS (cons true l1) (exist t1 (conj Hp Hl)))) => + (inright ? ? (HHH ?)) + | (inleft (existS _ _)) => (inright ? ? (HHH ?)) + | (inright Hnp) => (inright ? ? (HHH ?)) + end :: + {l'' : (list bool) & + {t : nat | (parse_rel (cons true l0) l'' t) /\ (le (length l'') (S (length l0)))}} + + {(l'' : (list bool)) (t : nat) ~ (parse_rel (cons true l0) l'' t)}). -- cgit v1.2.3