coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] How to talk about a restricted set of an inductive?

From: Robbert Krebbers <mailinglists AT robbertkrebbers.nl>
Cc: Fabien Renaud <Fabien.Renaud AT inria.fr>, coq-club AT inria.fr
Subject: Re: [Coq-Club] How to talk about a restricted set of an inductive?
Date: Thu, 03 Oct 2013 13:53:50 +0200

On 10/03/2013 01:49 PM, Robbert Krebbers wrote:

The best result you well get in this case is:

Goal forall A (l : list A) n, NList_ n l -> n <= length l.
Proof. induction 1; simpl; auto with arith. Qed.

... because

Goal forall A (l : list A) n, n <= length l -> NList_ n l.
Proof.
intros A l n; revert l. induction n as [|n]; [constructor|].
intros [|??]; simpl; [omega|]. constructor; auto with arith.
Qed.

[Coq-Club] How to talk about a restricted set of an inductive?, Fabien Renaud, 10/03/2013
- Re: [Coq-Club] How to talk about a restricted set of an inductive?, Rui Baptista, 10/03/2013
  - Re: [Coq-Club] How to talk about a restricted set of an inductive?, Fabien Renaud, 10/03/2013
    - Re: [Coq-Club] How to talk about a restricted set of an inductive?, Rui Baptista, 10/03/2013
      - Message not available
        
        Re: [Coq-Club] How to talk about a restricted set of an inductive?, Fabien Renaud, 10/03/2013
        
        Re: [Coq-Club] How to talk about a restricted set of an inductive?, Robbert Krebbers, 10/03/2013
        
        Re: [Coq-Club] How to talk about a restricted set of an inductive?, Robbert Krebbers, 10/03/2013
        Re: [Coq-Club] How to talk about a restricted set of an inductive?, Fabien Renaud, 10/03/2013
        Re: [Coq-Club] How to talk about a restricted set of an inductive?, Rui Baptista, 10/03/2013
        
        Re: [Coq-Club] How to talk about a restricted set of an inductive?, Cedric Auger, 10/03/2013
        
        Re: [Coq-Club] How to talk about a restricted set of an inductive?, Jonas Oberhauser, 10/04/2013
        Re: [Coq-Club] How to talk about a restricted set of an inductive?, Fabien Renaud, 10/04/2013
        Re: [Coq-Club] How to talk about a restricted set of an inductive?, Jean-Francois Monin, 10/04/2013
        Re: [Coq-Club] How to talk about a restricted set of an inductive?, Fabien Renaud, 10/04/2013
        
        Re: [Coq-Club] How to talk about a restricted set of an inductive?, Cedric Auger, 10/04/2013