The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

See 
https://coq.inria.fr/distrib/current/refman/language/cic.html#fixpoint-definitions 

>The main rules for being structurally smaller are the following.
>...

The termination checker reduces constants when needed, so it sees that 
False_ind is a match where all branches are smaller than lenp (since 
there are no branches ^^)


Gaëtan Gilbert

On 22/08/2019 17:56, Vincent Semeria wrote:
> Dear Coq clubbers,
>
> Consider this (silly) implementation of the subtraction of natural numbers :
>
> Fixpoint subtract (p n : nat) (lenp : le n p) { struct lenp }
>    : { k : nat | n + k = p }.
> Proof.
>    destruct (Nat.eq_dec n p) as [e|d].
>    - exists 0. subst p. rewrite Nat.add_0_r. reflexivity.
>    - destruct (subtract (pred p) n
>                         (match lenp in (_ <= n0) return (n <> n0 -> n <= 
> Init.Nat.pred n0) with
>                          | le_n _ => fun H : n <> n => False_ind (n <= 
> Init.Nat.pred n) (H eq_refl)
>                          | le_S _ m H1 => fun _ : n <> S m => H1
>                          end d)).
>      exists (S x). destruct p.
>      + exfalso. inversion lenp. subst n. exact (d (eq_refl _)).
>      + simpl in e. rewrite Nat.add_succ_r. apply f_equal. exact e.
> Defined.
>
> Is there a documentation somewhere explaining how the termination 
> checker is happy with it ? The only doc I found is this
> https://coq.inria.fr/distrib/current/refman/language/coq-library.html#index-19
> and it only tells that the type well_founded will terminate on 
> induction, not how it works.
>
> In subtract above, the recursive call is eventually made on a 
> structurally smaller piece of lenp, which is H1. But before getting H1, 
> the second branch of the match has to beta-reduce (fun _ => H1) d. Does 
> it only work with constant functions ?
>
> Also, the first branch of the match doesn't provide any smaller piece of 
> lenp. It is actually a dead branch, as shows False_ind. So the 
> termination checker is right to forget it, because it will never be 
> taken by computations. However I imagine that does require intelligence 
> in the checker, and I don't think that it simply tests the string 
> "False_ind".
>
> Regards,
> Vincent