The Coq mailing list

[Frédéric Dabrowski <frederic.dabrowski AT univ-orleans.fr>]

Thanks a lot. Now I know I should have looked at Equations earlier.

Best,

======================================================

Dr. Frédéric Dabrowski

Laboratoire d’Informatique Fondamentale d’Orléans

======================================================

Maître de conférences, Université d’Orléans, LIFO

Responsable. de l’équipe Langages Modèles et Vérification (LMV)

Site web : http://www.univ-orleans.fr/lifo/Members/Frederic.Dabrowski/

Téléphone :+33 (0)2 38 49 27 51

======================================================

Associate Professor, University of Orléans, LIFO

Head of the team Languages Models and Verification (LMV)

Home : http://www.univ-orleans.fr/lifo/Members/Frederic.Dabrowski/

Phone : +33 (0)2 38 49 27 51
======================================================

Le 3 avr. 2019 à 16:00, Yannick Forster <yannick AT yforster.de> a écrit :

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>
======================================================