Proof obligations, even on closed programs

[aa755]

Based on the description of the plugin in [1], I expected it to not need any user input when translating closed terms. However, sometimes, it leaves me with strange proof obligations.
Why does this happen? Is there a way to ensure that no user input is needed for closed terms?

Here is an example where user imput is needed:

Require Import NPeano.
Require Import Recdef.
Set Implicit Arguments.
Require Import Omega.

Function Gcd (a b : nat) {wf lt a} : nat :=
match a with
 | O => b 
 | S k =>  Gcd (b mod S k)  (S k)
end
.
Proof.
- intros m n k Heq. subst. apply Nat.mod_upper_bound.
  omega.
- exact lt_wf.
Defined.

Declare ML Module "paramcoq".

Parametricity Recursive Gcd.
intros.
destruct n.
- simpl. reflexivity.
- destruct m; simpl; reflexivity.
Parametricity Done.
... (* more obligations *)

[1] http://arxiv.org/abs/1209.6336

[mlasson]

Ok, so here is the problem with fixpoints.

A simplified version of the type rule of fixpoints is :

  F : A -> A
--------------
  fix  F : A

If you "translate" the premise, you obtain (where [|.|] is the translation):

  forall f1 f2, [|A|] f1 f2 -> [|A|] (F f1) (F f2)

Now, if you translate fixpoints:

[|F|] (fix F) (fix F) : [|A|] (fix F) (fix F) -> [|A|] (F (fix F)) (F (fix F)) 

If we would have F (fix F) === fix F (where === is definitionnal equality), then we could translate fixpoints by

[|fix F|] = fix ([|F|] (fix F) (fix F))

Unfortunately, F (fix F) === fix F does not hold (it would make coq definitional equality undecidable).
It does not hold definitionally but it most cases we can prove it propositionally, these are the "proof obligations" you get when translating fixpoint.

With "nice" fixpoints, there's a work-around to avoid all this "proof-obligation mess". A nice fixpoint is a fixpoint that is of the shape 'fixpoint f x1 ... xn (i : I y1 ... ym) := "nested match ... with ... with one of them destructing i". Note that all inductive principles are of this shape.

Finally, sometimes there's no way to get around these problems (the proof obligations are not provable).

Here is an example:

  Fixpoint zero (A : Type) (x : A) (p : x = x) := 0.

Try to convince yourself that you will not be able to prove (without axioms) that

  forall A x p, zero A x p = 0 

or

  forall A1 A2 AR x1 x2 xR p1 p2 pR, nat_R (zero A1 x1 x2 p1 p2 pR) (zero A1 x1 x2 p1 p2 pR).

[aa755]

Thanks Marc. Indeed, forall A x p, zero A x p = 0 seems impossible to prove without axioms. The only way to get that Fixpoint to compute is to make it's guard canonical (eq_refl). However, there is no way to show that p is propositionally equal to eq_refl.
Because there is no way to observe the body of zero in Coq's logic, it seems consistent to assume that the definition of zero is
something non parametric. Hence, the latter one seems unprovable too:
https://github.com/aa755/paramcoq/blob/v86FullNames/test-suite/dummyFix.v

However, I think that the this example (zero) is a pathological one.
Suppose Coq forced users to convert all non-recursive functions to use Definition instead of Fixpoint
(similarly, let instead of fix for inline non-recursive definitions). Then, would every closed term in Coq have a provable abstraction theorem?
If a fix is recursive (its body makes 1 of more recursive calls), even if it is non-nice, the guard term must be smaller in the recursive call. Thus, it seems possible to "destruct" the guard and hence observe that fix F = F (fix F).

Finally, I noticed that it helps to preprocess the branches of pattern matches to replace the occurrences of the dicriminee with appropriate constructors. For example, here is Nat.sub from the standard library:

Fixpoint sub (n m : nat) {struct n} : nat :=
  match n with
  | 0 => n (* bad. replace with 0 *)
  | S k => match m with
           | 0 => n (* bad. replace with (S k) *)
           | S l => sub k l
           end
  end

It seems that the translation described in the paper will produce something like:

Fixpoint sub_R (n₁ n₂ : nat) (n_R : nat_R n₁ n₂) (m₁ m₂ : nat) (m_R : nat_R m₁ m₂)
  {struct n_R} : nat_R (sub n₁ m₁) (sub n₂  m₂) :=
match n_R in nat_R n₁ n₂ return nat_R (sub n₁ m₁) (sub n₂ m₂) with  with 
| O_R => n_R (*type error. expecting nat_R 0 0, found nat_R n₁ n₂. this should be O_R*)
| S_R nr₁ nr₂ nr_R => ...
end.

which doesn't typecheck.
Indeed, invoking the parametricity plugin produces some obligations.
(these obligations are easily provable.)
Instead, after performing the replacements suggested above in sub, the plugin produces no obligations and the resultant sub_R is very simple:

Fixpoint sub (n m : nat) {struct n} : nat :=
  match n return  nat with
  | 0 => 0 (* originally n*)
  | S k => match m return nat with
           | 0 => S k (* originally n*)
           | S l => sub k l
           end
  end.

Perhaps we can do this preprocessing before translating matches? Is there already a function in Coq's plugin API to do this kind of preprocessing?

[herbelin]

Hi, what is the current status of the Fixpoint zero (A : Type) (x : A) (p : x = x) := 0. example? I thought at first that it was about dummy fixpoints but it seems after all to be more generally about non-linear constraints on indices occurring inside the proper context of the fixpoint. For instance, for

Inductive eq : nat -> nat -> Type :=
  | refl0 : eq 0 0
  | reflS x : eq x x -> eq (S x) (S x).

I could prove:

Fixpoint f x y (p : eq x y) :=
  match p with
  | refl0 => 0
  | reflS x p => f x x p end.

Theorem f_spec x y p : f x y p = 0.

but not:

Fixpoint f' x (p : eq x x) :=
  match p with
  | refl0 => 0
  | reflS x p => f' x p end.

Theorem f'_spec x p : f' x p = 0.

I wonder whether there is a general rule to characterize these fixpoints, or, alternatively, if there is a way to type fix so that either they are rejected or the theorems are probable.

[proux01]

Hi, what is the current status of the Fixpoint zero (A : Type) (x : A) (p : x = x) := 0. example?

I would say: same status as five years ago, when this was opened.