The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

Hi Arthur,

  It is “reasonable” in the sense that a match with no branch (the match f 
with end)
indicates an unreachable program fragment. The fact that it’s hidden under a 
lambda
makes the whole argument “reachable” though, but not in constructor form, so 
the
recursive call to contradiction will never fire, this application is stuck 
(you
have to "think in call-by-value" for recursive calls).
  
  I’d be curious to know what justifies that we can consider this empty match 
under 
a lambda a subterm though. If you think of the well-founded version of this, 
the
order on unit is the empty relation, and the obligation at the recursive call
would be (match Heq in … with eq_refl => fun f => match f with end end < tt), 
which you couldn’t prove without having already a contradiction in your 
context, 
as far as I know.

Best,
— Matthieu

On 12 déc. 2013, at 19:12, Arthur Azevedo de Amorim 
<arthur.aa AT gmail.com>
 wrote:

> On Dec 12, 2013 2:12 PM, "Arthur Azevedo de Amorim" 
> <arthur.aa AT gmail.com>
>  wrote:
> Wow, I'm really impressed that the termination checker accepts the 
> definition of  contradiction... Why is this reasonable?
> 
> On Dec 12, 2013 2:02 PM, "Daniel Schepler" 
> <dschepler AT gmail.com>
>  wrote:
> Section func_unit_discr.
> 
> Hypothesis Heq : (False -> False) = unit :> Type.
> 
> Fixpoint contradiction (u : unit) : False :=
> match u with
> | tt => contradiction (
>         match Heq in (_ = T) return T with
>         | eq_refl => fun f:False => match f with end
>         end
>         )
> end.
> 
> End func_unit_discr.
> 
> Definition func_unit_discr :
>   (False -> False) <> unit :> Type :=
> fun Heq => contradiction Heq tt.
> 
> Section bijective_impl_eq.
> 
> Definition injective {A B:Type} (f:A->B) : Prop :=
> forall x y:A, f x = f y -> x = y.
> 
> Definition surjective {A B:Type} (f:A->B) : Prop :=
> forall y:B, exists x:A, f x = y.
> 
> Definition bijective {A B:Type} (f:A->B) : Prop :=
> injective f /\ surjective f.
> 
> Hypothesis bijective_impl_eq :
>   forall (A B:Type) (f:A->B), bijective f -> A = B.
> 
> Hypothesis functional_extensionality :
>   forall (A B:Type) (f g:A->B),
>   (forall x:A, f x = g x) -> f = g.
> 
> Lemma unit_eq_False_False_funs :
>   (False -> False) = unit :> Type.
> Proof.
> apply bijective_impl_eq with (f := fun _ => tt).
> split.
> + intros f g ?.
>   apply functional_extensionality.
>   intros [].
> + intros [].
>   exists (fun f:False => match f with end).
>   reflexivity.
> Qed.
> 
> Definition not_bijective_impl_eq : False :=
> func_unit_discr unit_eq_False_False_funs.
> 
> End bijective_impl_eq.
> -- 
> Daniel Schepler
>