The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

Notice that "dependent destruction" silently assumes the "JMeq_eq" 
axiom. This lemma can also be proven without axioms by using an 
appropriate return clause in your match.

Require Import Program.

Inductive t2 : nat -> Prop :=
| A2 : t2 0
| B2 : t2 1.

Lemma toto2 : forall (x:t2 0), x = A2.
Proof.
  dependent destruction x ; auto.
Qed.

Print Assumptions toto2.
(* Axioms: JMeq_eq *)

Lemma toto2_alt : forall (x:t2 0), x = A2.
Proof.
  exact (fun x =>
    match x as x' in t2 n return
      match n with
      | 0 => fun x' => x' = A2
      | S _ => fun _ => True
      end x'
    with A2 => eq_refl | B2 => I end).
Qed.

Print Assumptions toto2_alt.
(* Closed under the global context *)

On 12/06/2012 12:29 PM, Vincent BENAYOUN wrote:
> Thank you Greg for your answer.
>
> Vincent
>
>
> 2012/12/3 Greg Morrisett 
> <greg AT eecs.harvard.edu
> <mailto:greg AT eecs.harvard.edu>>
>
>     The easiest thing is to use "dependent destruction" from the
>     Program library:
>
>     Require Import Program.
>
>     Inductive t2 : nat -> Prop :=
>     | A2 : t2 0
>     | B2 : t2 1.
>
>     Lemma toto2 : forall (x:t2 0), x = A2.
>     Proof.
>        dependent destruction x ; auto.
>     Qed.
>
>     -Greg
>
>     On Dec 3, 2012, at 8:41 AM, Vincent BENAYOUN
>     
> <benayoun.vincent AT gmail.com
>  
> <mailto:benayoun.vincent AT gmail.com>>
>  wrote:
>
>      > Thank you very much for your answer.
>      > I understand the error message but I still can't find a way to
>     solve my problem.
>      > Thanks to your explanations, I managed to explain more precisely
>     my problem as follow.
>      >
>      > For the following Lemma, I would like to prove it by induction
>     but I can't because of the type error. Well, a can give a proof term.
>      >
>      > Inductive t : nat -> Prop :=
>      > | A : t 0.
>      >
>      > Lemma toto : forall (x:t 0), x = A.
>      > Proof.
>      >   intro x.
>      >   apply(match x with | A => eq_refl end).
>      > Qed.
>      >
>      >
>      > But since there are many cases, I don't know how to prove the
>     Lemma. The following Coq script fails with a type error.
>      >
>      >
>      > Inductive t2 : nat -> Prop :=
>      > | A2 : t2 0
>      > | B2 : t2 1.
>      >
>      > Lemma toto2 : forall (x:t2 0), x = A2.
>      > Proof.
>      >   intros x.
>      >   eapply(match x with | A2 => eq_refl | B2 => _ end).
>      > Qed.
>      >
>      > I should prove False in the second branch of the pattern-matching
>     but I don't know how !
>      > Is there a way to prove such a Lemma ?
>      >
>      > Thanks in advance,
>      > Vincent
>      >
>      >
>      >
>      > 2012/11/29 Arnaud Spiwack 
> <aspiwack AT lix.polytechnique.fr
>     
> <mailto:aspiwack AT lix.polytechnique.fr>>
>      > Well, the problem is as explained in the error message: it
>     produces a type error.
>      >
>      > First note that induction x eqn:e can be broken down into
>     remember x eqn:e; induction x.
>      >
>      > Rewriting your file as
>      >
>      > Inductive bbb : nat -> Prop :=
>      > | BBB : bbb 0.
>      >
>      > Lemma bbb_theorem :
>      >   forall (n:nat), bbb n -> n = 0.
>      > Proof.
>      >   intros n HHH.
>      >   remember HHH eqn:toto.
>      >   induction HHH.
>      >   reflexivity.
>      > Qed.
>      >
>      > Before the induction step we have the following goal:
>      >
>      > n : nat
>      > HHH : bbb n
>      > b : bbb n
>      > toto : b = HHH
>      > ______________________________________(1/1)
>      > n = 0
>      >
>      > Now, doing induction on HHH tries to create the term:
>      >
>      > fun n' : nat => forall b : bbb n', b = HHH -> n' = 0
>      >
>      > The "fun n' =>" part is to be able to substitute n with the
>     correct value for the required constructor. It also puts toto back
>     as an implication (you can do it with: revert toto). The problem
>     here is obvious: b has type bbb n' and HHH has type bbb n which are
>     different, hence b=HHH isn't well-typed. And the tactic fails.
>      >
>      > Instead you can do  elim HHH, which works like induction HHH but
>     without doing any revert. But of course, in that case, your
>     remembered equation will be useless.
>      >
>      >
>      >
>      > On 28 November 2012 11:55, Vincent BENAYOUN
>     
> <benayoun.vincent AT gmail.com
>  
> <mailto:benayoun.vincent AT gmail.com>>
>  wrote:
>      > Inductive bbb : nat -> Prop :=
>      > | BBB : bbb 0.
>      >
>      > Lemma bbb_theorem :
>      >   forall (n:nat), bbb n -> n = 0.
>      > Proof.
>      >   intros n HHH.
>      >   induction HHH eqn:toto.
>      >   reflexivity.
>      > Qed.
>      >
>      >