1
(* Check the synthesis of predicate from a cast in case of matching of
2
the first component (here [list bool]) of a dependent type (here [sigS])
3
(Simplification of an example from file parsing2.v of the Coq'Art
8
Variable parse_rel : list bool -> list bool -> nat -> Prop.
10
Variables (l0 : list bool)
12
forall l' : list bool,
13
length l' <= S (length l0) ->
15
{t : nat | parse_rel l' l'' t /\ length l'' <= length l'}} +
16
{(forall (l'' : list bool) (t : nat), ~ parse_rel l' l'' t)}).
18
Axiom HHH : forall A : Prop, A.
21
(match rec l0 (HHH _) with
22
| inleft (existS (false :: l1) _) => inright _ (HHH _)
23
| inleft (existS (true :: l1) (exist t1 (conj Hp Hl))) =>
25
| inleft (existS _ _) => inright _ (HHH _)
26
| inright Hnp => inright _ (HHH _)
29
{t : nat | parse_rel (true :: l0) l'' t /\ length l'' <= S (length l0)}} +
30
{(forall (l'' : list bool) (t : nat), ~ parse_rel (true :: l0) l'' t)}).
32
(* The same but with relative links to l0 and rec *)
36
(rec : forall l' : list bool,
37
length l' <= S (length l0) ->
39
{t : nat | parse_rel l' l'' t /\ length l'' <= length l'}} +
40
{(forall (l'' : list bool) (t : nat), ~ parse_rel l' l'' t)}) =>
41
match rec l0 (HHH _) with
42
| inleft (existS (false :: l1) _) => inright _ (HHH _)
43
| inleft (existS (true :: l1) (exist t1 (conj Hp Hl))) =>
45
| inleft (existS _ _) => inright _ (HHH _)
46
| inright Hnp => inright _ (HHH _)
49
{t : nat | parse_rel (true :: l0) l'' t /\ length l'' <= S (length l0)}} +
50
{(forall (l'' : list bool) (t : nat), ~ parse_rel (true :: l0) l'' t)}).