The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Oooh, nice!

Something strange seems to be going on here, though.  Why does this not replace H1 with eq_refl?

Goal forall (T : Type) (feq : Eq=Eq->T) (H1 : Eq=Eq), feq eq_refl = feq H1.

  intros.

  revert dependent H1.

  refine (fun H1 => match H1 with eq_refl => _ end).

On Wed, Aug 17, 2016 at 2:54 PM Hugo Herbelin <Hugo.Herbelin AT inria.fr> wrote:

Hi,

There is indeed a (limited) use of "small inversion" (see
e.g. Jean-François Monin's "Proof Trick: Small Inversion", see also
CPDT, etc.) in the inference of the return clause. Namely, let t be of
type I a1 ... an u1 ... um, with the ai parameters of some inductive
type I and the uj indices for this inductive type. Assume that each uj
can be decomposed under the form pj(vj1..vjqj) exposing patterns pj
and non-patterns vjk at the leaves of the patterns. Then, a matching
on t will try to infer a return clause of the form

   as y
   in I _ ... _ x1 ... xp
   return match x1, ..., xp, y with
          | p1(z11,...,z1q1), ..., pm(zm1,...,zmqm, w => ?T@{z11:=z11,..,zmqm:=zmqm,w:=w}
          | _ => IDProp
          end

together with the constraint ?T@{z11:=v11,..,zmqm:=vmqm,w:=t}
convertible with the expected type of the match.

In the case of "H : Eq = Eq", i.e. I is "eq", the parameters are
"comparison" and "Eq", the unique index is "Eq", so a return clause of
the following form (*)

   as H2
   in _ = x
   return match x, H2 with
          | Eq, w => ?T@{w}
          | _ => IDProp
          end

is used, together with the constraint ?T@{w:=H} convertible to
"feq eq_refl = feq H", for which the solution ?T@{w} :=
"feq eq_refl = feq w" is eventually found.

Now, because x is dependent in the type of H, a generalization is
automatically performed to compile (*), leading to

  as H2
  in (_ = c)
  return
     match c as x return (Eq = x -> Type) with
     | Eq => fun w : Eq = Eq => feq eq_refl = feq w
     | Lt => fun _ : Eq = Lt => IDProp
     | Gt => fun _ : Eq = Gt => IDProp
     end H2

as shown by Jason.

As noticed by Jonathan, this does not work for "H : b = b" with b a
variable in bool because there is no pattern structure in b (one would
need first to do a "destruct b"). Only the pattern structure of
indices is exploited.

Combined with induction, the method can be used to prove UIP for nat
(a proof for nat can be found in Eqdep_dec.UIP_refl_nat).

I did not follow all what has been done recently, and maybe someone
like Jean-François knows the general rule, or maybe Conor McBride, but
that would indeed be very nice, and an interesting exercice, that this
method be made formal and be generalized to mechanically prove UIP for
first-order inductive types in Set (and eventually to all types built
from inductive types in Set and arrow, using functional
extensionality, if I'm correct, inspired by the interpretation of Set
as hset).

Best,

Hugo

Note 1: IDProp := "forall P:Prop, P -> P" is used because it is the
simplest non-inductive type which we now how to inhabit.

Note 2: Work was done recently by Meven Bertrand on how to use small
inversion also in the inference of the inner return clauses of a
nested pattern-matching problem. I hope this will eventually come into
the code and increase further the strength of the pattern-matching
algorithm.

On Wed, Aug 17, 2016 at 04:10:17PM -0400, Jean-Marie Madiot wrote:
> More precisely (my guess is) that it works when "being equal to the given
> *element* of the type" is decidable (or more simply, can be done with a finite
> pattern matching term).
>
> For exemple, equality on streams is not decidable, but we can decide equality
> to a finite stream.  And the same refine tactic works.  However, try it with an
> infinite stream, and it fails to help.
>
>
> CoInductive stream :=
>   | nil : stream
>   | cons : nat -> stream -> stream.
>
> Lemma test1 :
>   forall (T : Type)
>     (feq : cons 3 nil = cons 3 nil -> T)
>     (H1 : cons 3 nil = cons 3 nil),
>     feq eq_refl = feq H1.
> Proof.
>   intros T feq H.
>   refine (match H with eq_refl _ => _ end).
>   reflexivity.
> Qed.
>
> Lemma test2 :
>   forall (T : Type)
>     (feq : (cofix x := cons 3 x) = (cofix x := cons 3 x) -> T)
>     (H1 : (cofix x := cons 3 x) = (cofix x := cons 3 x)),
>     feq eq_refl = feq H1.
> Proof.
>   intros T feq H.
>   Fail progress refine (match H with eq_refl _ => _ end).
> Abort.
>
>
>
> On Wed, Aug 17, 2016 at 3:55 PM, Jason Gross <jasongross9 AT gmail.com> wrote:
>
>     It only works if the type has decidable equality.  list nat has decidable
>     equality.   It is also decidable whether or not a list of any type is nil,
>     or not.  If you instead try (feq : Set::nil = Set::nil -> T), you will find
>     that it does not work.  If you try (feq : Set = Set -> T) it will not
>     work.  If you try (feq : list nat = list nat -> T), it will not work.  If
>     you try (feq : S = S -> T) it will not work.  If you try (feq : eq_refl 0 =
>     eq_refl 0 -> T), it may or may not work (this still has decidable equality,
>     but it is more complicated).
>
>     On Wed, Aug 17, 2016 at 12:04 PM Soegtrop, Michael <
>     michael.soegtrop AT intel.com> wrote:
>
>         Dear Jason, Jonathan,
>
>         thanks for the solution and explanation.
>
>         I experimented a bit. I think that this works for any literal term of
>         any type, even if it doesn't have decidable equality. E.g.:
>
>         Open Scope list_scope.
>
>         Lemma TestNatList: forall (T : Type) (feq : 3::nil=3::nil->T) (H1 :
>         3::nil=3::nil), feq eq_refl = feq H1.
>         Proof.
>           intros.
>           refine (match H1 with
>                   | eq_refl _ => _
>                   end).
>           reflexivity.
>         Qed.
>
>         The resulting proof term is lengthy. I guess the decidable equality is
>         required if the value compared is not a literal, but a parameter.
>
>         Best regards,
>
>         Michael
>         Intel Deutschland GmbH
>         Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
>         Tel: +49 89 99 8853-0, www.intel.de
>         Managing Directors: Christin Eisenschmid, Christian Lamprechter
>         Chairperson of the Supervisory Board: Nicole Lau
>         Registered Office: Munich
>         Commercial Register: Amtsgericht Muenchen HRB 186928
>
>