Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] induction on arbitrary-arity trees

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] induction on arbitrary-arity trees


chronological Thread 
  • 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











Archive powered by MhonArc 2.6.16.

Top of Page