The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

I thought the termination analyser for fix only allowed recursive calls on strict sub-terms of the decreasing argument.

In the definition of contradiction, there is only one argument u, and there are no sub-terms of tt. I don't see how the termination analyser accepted the recursive call in this definition.

Is this a bug in the termination analysis for fix, or I am missing something?

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Thu, Dec 12, 2013 at 2:51 PM, Matthieu Sozeau <matthieu.sozeau AT gmail.com> wrote:

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
>