The Coq mailing list

[Gaetan Gilbert <gaetan.gilbert AT ens-lyon.fr>]

>For instance, one can prove forall (x:True), x = I, but not:
>
>Inductive Foo : unit -> Prop := foo : Foo tt.
>
>Goal forall (f : Foo tt), f = foo.

You can actually.


Inductive Foo : unit -> Prop := foo : Foo tt.

Definition foo_transport : forall (x : unit) (y : unit), Foo x -> Foo y.
Proof.
intros [] [];trivial.
Defined.

Goal forall (f : Foo tt), f = foo.
Proof.
assert (H : forall x y (a : Foo x) (b : Foo y), foo_transport _ _ a = b).
intros x y [] [].
reflexivity.
intros.
etransitivity.
- symmetry. apply H.
- apply H.
Unshelve.
+ exact tt.
+ exact f.
Defined.

Gaëtan Gilbert

On 07/09/2016 18:21, Jonathan Leivent wrote:
> On 09/07/2016 10:13 AM, Soegtrop, Michael wrote:
> > Dear Guillaume,
> >
> > > Coq just checks that this is true for all the branches  of the 
> > > "match"; if so, it assumes that it is also true for the "match" itself.
> > Sorry, I don't get it. That is what I assumed Coq does until I saw 
> > your example, but how does Coq check that (in my example below ) the 
> > branch term "1" has type "bool"?
> >
> > Definition foo2 (H : nat = bool) : bool :=
> >    match H in (_ = t) return t with
> >    | eq_refl => 1
> >    end.
>
> Here's a non-type-theorists view of what is happening: matches on 
> equalities can only reduce when the equality is exactly eq_refl 
> because otherwise the equality might be hypothetical - as in your nat 
> = bool case.  Even assuming UIP, when there can only be one proof of 
> the equality, there can also be no proof of it.  Hence, what the match 
> above says is : in the imaginary world where we can prove nat = bool, 
> 1 is a bool because it is a nat.
>
> IMHO, the more interesting "feature" about Coq's logic is that it 
> doesn't have universal UIP - hence it can't even assume an actual 
> proof of x = x is always eq_refl, even though eq_refl is the only way 
> to construct x = x.  And, other constructive-logic-based 
> dependently-typed languages out there, such as Agda and Idris, do have 
> UIP built in (via K, which is equivalent).  Coq seems to act in 
> confusing ways when dealing with x = x.  Sometimes, when that x = x is 
> alone, it can reduce it to eq_refl.  Other times, when there are 
> multiple instances of x = x in a goal, it can only reduce one to 
> eq_refl.  Also, other one-constructor fieldless Props are irrelevant  
> - as long as they don't have a type index.
>
> For instance, one can prove forall (x:True), x = I, but not:
>
> Inductive Foo : unit -> Prop := foo : Foo tt.
>
> Goal forall (f : Foo tt), f = foo.
>
>
> -- Jonathan