coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Christine Paulin <Christine.Paulin AT lri.fr>
- To: David Monniaux <David.Monniaux AT ens.fr>
- Cc: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] induction on arbitrary-arity trees
- Date: Thu, 31 Mar 2005 13:08:48 +0200
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
You need to define an apropriate induction principle for instance
Fixpoint comp_widening_chain_rec2
(S : Set) (P : comp_widening_chain S -> Type)
(f : forall (x : S) (o : S -> option (comp_widening_chain S)),
(forall (s:S), match (o s) with Some u => P u | None => True end)
-> P (comp_widening_chain_intro S x o))
(c : comp_widening_chain S) {struct c} : (P c) :=
match c as c0 return (P c0) with
| comp_widening_chain_intro x o => f x o
(fun (s:S) => match (o s) as c0
return match c0 with Some u => P u | None => True end
with Some u => comp_widening_chain_rec S P f u
| None => I
end)
end.
and use elim c using comp_widening_chain_rec2
Another possibility for expressing the recursive hypothesis mimics the
equivallent mutually recursive definition.
It would have type
(S : Set) (P : comp_widening_chain S -> Type)
(P1 : option (comp_widening_chain S) -> Type)
(f : forall (x : S) (o : S -> option (comp_widening_chain S)),
(forall (s:S), P1 (o s))
-> P (comp_widening_chain_intro S x o)))
(f1 : forall (u:comp_widening_chain S), (P u) -> (P1 (Some u)))
(f2 : (P1 None))
(c : comp_widening_chain S) -> (P c)
P and P1 should be proved by mutual recursion and used via the tactic
elim c using elim_lemma with P1 := ...
We see on this example that stating the apropriate induction principle
for this kind of nested inductive definition is not very natural.
This is the reason why the Coq system only generates a week principle,
letting the user choose the best-suited principle for his/her
particular problem ...
Christine Paulin
David Monniaux writes:
> I have the following definition:
>
> Inductive comp_widening_chain (S : Set) : Set :=
> comp_widening_chain_intro : forall x : S,
> (forall y : S,
> (option (comp_widening_chain S))) -> (comp_widening_chain S).
>
> If I try to do reasonings by induction using the "induction" or "elim"
> on such a datatype, I don't get an induction hypothesis.
>
> I'm forced to use
>
> refine (fix inductive_predicate (foobar : comp_widening_chain) : ... := _)
>
> But that's clunky, and, I'm afraid, this seems to lead to weird error
> messages (see other mail).
>
> What is the correct way of doing induction on such things?
>
> Regards,
> DM
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
> http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
--
Christine Paulin-Mohring mailto :
Christine.Paulin AT lri.fr
LRI, UMR 8623 CNRS, Bat 490, Université Paris Sud, 91405 ORSAY Cedex
tel : (+33) (0)1 69 15 66 35 fax : (+33) (0)1 69 15 65 86
- [Coq-Club] induction on arbitrary-arity trees, David Monniaux
- Re: [Coq-Club] induction on arbitrary-arity trees, Christine Paulin
- Re: [Coq-Club] induction on arbitrary-arity trees, Hugo Herbelin
Archive powered by MhonArc 2.6.16.