coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] dependent induction 2

From: Pierre Courtieu <Pierre.Courtieu AT cnam.fr>
To: Andrew Polonsky <andrew.polonsky AT gmail.com>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] dependent induction 2
Date: Fri, 24 Feb 2012 11:07:04 +0100
Authentication-results: mr.google.com; spf=pass (google.com: domain of pierre.courtieu AT gmail.com designates 10.204.149.198 as permitted sender) smtp.mail=pierre.courtieu AT gmail.com; dkim=pass header.i=pierre.courtieu AT gmail.com

Hello, here is a script proving your goal in v8.3 and v8.4 (14975). It
makes use of JMeq but the statement of the lemma is the one you want.

Tactic dependent generalize_eqs_vars does not seem to be documented
but one should be able to do the same by hand.

Bests
P.C.
------------8X-------------------
Require Export JMeq.

Variable A:Type.
Variable F: A -> A.
Inductive graF : A -> A -> Type := io_pair (a:A) : graF a (F a).

Goal forall (a:A) (g: graF a (F a)), g = (io_pair a).
intros a g.
dependent generalize_eqs_vars g.
intros g0 H H0.
induction g.
apply JMeq_eq.
auto.
Qed.

[Coq-Club] dependent induction 2, Andrew Polonsky
- Re: [Coq-Club] dependent induction 2, Arnaud Spiwack
  - Re: [Coq-Club] dependent induction 2, Nils Anders Danielsson
    - Re: [Coq-Club] dependent induction 2, Arnaud Spiwack
      - Message not available
        
        Re: [Coq-Club] dependent induction 2, Arnaud Spiwack
- Re: [Coq-Club] dependent induction 2, Pierre Courtieu
  - Re: [Coq-Club] dependent induction 2, Adam Chlipala
    - Re: [Coq-Club] dependent induction 2, Pierre Courtieu
  - Re: [Coq-Club] dependent induction 2, Vincent Siles
    - Re: [Coq-Club] dependent induction 2, Andrew Polonsky