The Coq mailing list

[Yannick Forster <yannick AT yforster.de>]

Equations can indeed do it quite easily:


From Equations Require Import Equations.

Inductive eType : Set := Integer | Boolean.

Inductive unop : eType -> Type :=
  Neg : unop Integer
| Not : unop Boolean.

Derive NoConfusion for eType.

Lemma a : forall x : unop Integer, x = Neg.
Proof.
  intros. dependent elimination x. reflexivity.
Qed.
Print Assumptions a.


This gives "Closed under the global context" (at least on beta2 and 
master). The proof term will be a bit more convoluted than the one using 
match, but in bigger proofs that shouldn't matter.

Best,
Yannick

--
PhD student, Programming Systems Lab, Saarland University
https://www.ps.uni-saarland.de/~forster/


On 03/04/2019 15:39, Gaëtan Gilbert wrote:
> 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>
> > > > ======================================================