The Coq mailing list

[Andreas Abel <andreas.abel AT ifi.lmu.de>]

On 22.11.12 9:51 AM, AUGER Cédric wrote:
> > Variable pi_refl : h = h'.
> > Definition p : g h = false
> >     := resp h h' pi_refl.
> >
> > (* If we have proof irrelevance, then pi_refl can be replaced by
> > eq_refl. But then p reduces to eq_refl, but eq_refl does not have
> > type g h = false,
> >      because g h does not reduce.
> >
> >      Subject reduction is lost (once more).
> >    *)
>
> I doubt you find it interesting, and it does not mean much, but I
> instantiated pi_refl, to see what would be the outputs.
>
> Definition pi_refl : h = h'.
>    exact ((eq_refl h : (h:Acc R 1:Prop) = (h:Acc R 1:Prop))
>          : (h:Acc R 1:Prop) = (h':Acc R 1:Prop)).
> Defined.
> Print pi_refl.
> (*
> pi_refl =
> (eq_refl
>   :(h:Acc R 1:Prop) = (h:Acc R 1:Prop))
> :(h:Acc R 1:Prop) = (h':Acc R 1:Prop)
>       : h = h'
> *)
> Definition p : g h = false
>     := resp h h' pi_refl.
>
> Eval compute in p.
> (*
>       = eq_refl
>       : g h = false
> *)

That is exactly the point, because if you

  Check (eq_refl : g h = false)

then Coq (including your version) will say no.

Cheers,
Andreas

--
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel AT ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/