The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

The Equations plugin should be able to do it today
or you can "dependent induction x" today, however this uses an axiom

Gaëtan Gilbert

On 03/04/2019 15:22, Frédéric Dabrowski wrote:
> Thanks Vincent and Gaetan
>
> So it is because of Integer that I can’t perform a dependent inversion.
> Do you thinks there is any chance that dependent inversion will be able 
> to deal with this some day?
>
> Best regards,
> F.
>
>
> ======================================================
>
> Dr. Frédéric Dabrowski
> Laboratoire d’Informatique Fondamentale d’Orléans 
> <https://www.univ-orleans.fr/lifo/>
>
> ======================================================
> Maître de conférences, Université d’Orléans, LIFO
> Responsable. de l’équipe Langages Modèles et Vérification 
> <http://www.univ-orleans.fr/lifo/equipes/LMV/?Home> (LMV)
>
> Site web : http://www.univ-orleans.fr/lifo/Members/Frederic.Dabrowski/
> Téléphone :+33 (0)2 38 49 27 51 <tel:+33(0)238492751>
> ======================================================
> Associate Professor, University of Orléans, LIFO
> Head of the team Languages Models and Verification 
> <http://www.univ-orleans.fr/lifo/equipes/LMV/?Home>(LMV)
>
> Home : http://www.univ-orleans.fr/lifo/Members/Frederic.Dabrowski/
> Phone : +33 (0)2 38 49 27 51 <tel:+33(0)238492751>
> ======================================================
>
> > Le 3 avr. 2019 à 15:13, Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net 
> > <mailto:gaetan.gilbert AT skyskimmer.net>> a écrit :
> >
> > Coq will automatically do small inversion when pattern matching, so 
> > this works:
> > Definition a (x:unop Integer) : x = Neg :=
> >  match x with Neg => eq_refl end.
> > you can "Print a." to see what it generates
> >
> > If you want to do it by hand the idea is to generalize your statement 
> > so that the thing you match on has indices which are independent 
> > variables, and when instantiated properly it implies what you want
> >
> > For instance
> >
> > Lemma a : forall x : unop Integer, x = Neg.
> > Proof.
> >  assert (forall t (x:unop t), x = match t with Integer => Neg | 
> > Boolean => Not end).
> >  { intros t x;destruct x;reflexivity. }
> >  intros x;apply (H Integer).
> > Qed.
> >
> > or
> >
> > Lemma a : forall x : unop Integer, x = Neg.
> > Proof.
> >  assert (forall t (x:unop t), match t with Integer => fun x => x = Neg 
> > | Boolean => fun _ => True end x).
> >  { intros t x;destruct x;reflexivity. }
> >  intros x;apply (H Integer).
> > Qed.
> >
> > Gaëtan Gilbert
> >
> > On 03/04/2019 15:01, Frédéric Dabrowski wrote:
> > > Dear all,
> > > I’m stuck with the following simple example for which I did not 
> > > expect to spend more than 5 seconds …
> > > How do I remove this ugly Admitted?
> > > Best regards,
> > > Inductive eType : Set := Integer | Boolean.
> > > Inductive unop : eType -> Type :=
> > >   Neg : unop Integer
> > > | Not : unop Boolean.
> > > Lemma a : forall x : unop Integer, x = Neg.
> > > Proof.
> > > Admitted.
> > > ======================================================
> > > Dr. Frédéric Dabrowski
> > > Laboratoire d’Informatique Fondamentale d’Orléans 
> > > <https://www.univ-orleans.fr/lifo/>
> > > ======================================================
> > > Maître de conférences, Université d’Orléans, LIFO
> > > Responsable. de l’équipe Langages Modèles et Vérification 
> > > <http://www.univ-orleans.fr/lifo/equipes/LMV/?Home> (LMV)
> > > Site web : http://www.univ-orleans.fr/lifo/Members/Frederic.Dabrowski/
> > > Téléphone :+33 (0)2 38 49 27 51 <tel:+33(0)238492751>
> > > ======================================================
> > > Associate Professor, University of Orléans, LIFO
> > > Head of the team Languages Models and Verification 
> > > <http://www.univ-orleans.fr/lifo/equipes/LMV/?Home>(LMV)
> > > Home : http://www.univ-orleans.fr/lifo/Members/Frederic.Dabrowski/
> > > Phone : +33 (0)2 38 49 27 51 <tel:+33(0)238492751>
> > > ======================================================