Structural recursion on Prop

Stream: Type theory

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

I have been trying to understand the Bove-Capretta encoding of partial recursive functions in Rocq. The basic idea is that for a specific function, one builds an inductive predicate representing either the call graph or the domain of this function, but in either case does so in a way that follows the structure of recursive calls. Then to define the function, we simply proceed by structural recursion on the predicate. This is well and good, but the bizarre thing (to me) is that in Rocq, the predicate can live in Prop.

For example, in section 15.4 of Bertot and Castéran, the log function is defined. The OCaml pseudocode is

let rec log x = match x with
  S 0 -> 0
| S (S p) -> S (log (S (div2 p)))

To define this, we first specify when an input lives in the domain of log:

Inductive log_domain : nat -> Prop :=
  log_domain_1 : log_domain 1
| log_domain_2 : ∀p : nat, log_domain (S (div2 p)) -> log_domain (S (S p)).

Then, after proving some inversion theorems (which must be defined in such a way that the output is "smaller" than the input; essentially the output is an argument to the input constructor; a "blatant violation of the principle of proof irrelevance"), we define

Fixpoint log (x:nat) (h:log_domain x) {struct h} : Nat := ...

The key thing here is {struct h}, telling Fixpoint to proceed by structural recursion on h. A more complicated example is here.

In Lean this pretty obviously cannot work: log_domain is not a syntactic subsingleton, so subsingleton elimination doesn't apply and the generated recursor can only eliminate into Prop. The question is: why does this make sense in Rocq? Why is it consistent with proof irrelevance? I would be grateful for any expert weighing in here.

One clue is that Rocq has pattern matching (case?) and fixpoints built into the type theory, I think as distinct elimination forms. Is it then the case that while one cannot match on proofs when eliminating into data, recursion into data is foundationally a different concept and is allowed?

Adding to my confusion is this SO answer which seems to suggest that the difference has something to do with whether proof irrelevance is definitional (like in Lean, or Rocq's SProp) or axiomatic (like in Rocq's Prop). While we know from #leantt that this difference does impact normalization and metatheory, I am not seeing why it matters here.

[Mario Carneiro]

I think log_domain can be considered a syntactic subsingleton by a more permissive check. The important property is that all the non-prop data in the constructor (which constructor, and the argument p to the second one) can be constructed from inversion on the index.

[Mario Carneiro]

You can presumably prove that this type is a subsingleton in Rocq as a result

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Ok, it cannot be the "fiberwise subsingleton" property that makes this work; I verified that Rocq still accepts this definition if you use

Inductive log_domain : nat -> Prop :=
  log_domain_1 : log_domain 1
(* Can even put a bunch of data there if we want. *)
| log_domain_1a : nat -> log_domain 1
| log_domain_2 : forall p:nat, log_domain (S (Nat.div2 p)) -> log_domain (S (S p)).

[Mario Carneiro]

what exactly is your Fixpoint?

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Here is the full example from Bertot/Castéran:

Inductive log_domain : nat -> Prop :=
  log_domain_1 : log_domain 1
| log_domain_2 : forall p:nat, log_domain (S (Nat.div2 p)) -> log_domain (S (S p)).

Theorem log_domain_non_0 : forall x:nat, log_domain x -> x <> 0.
Proof.
  intros x H; case H; intros; discriminate.
Qed.

Theorem log_domain_inv : forall x p:nat, log_domain x -> x = S (S p) -> log_domain (S (Nat.div2 p)).
Proof.
  intros x p H; case H; try (intros H'; discriminate H').
  intros p' H1 H2; injection H2; intros H3; rewrite <- H3; assumption.
Defined.

Fixpoint log (x:nat) (h:log_domain x) {struct h} : nat :=
  match x as y return x = y -> nat with
  | 0 => fun h' => False_rec nat (log_domain_non_0 x h h')
  | S 0 => fun h' => 0
  | S (S p) => fun h' => S (log (S (Nat.div2 p)) (log_domain_inv x p h h'))
  end (refl_equal x).

[Mario Carneiro]

and when you have two log_domain_1's you just get more cases in the inversion lemma?

[Mario Carneiro]

actually can you show that version?

[Mario Carneiro]

Are you actually using log_domain_1a in the inversion lemma?

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Sorry I removed it, but here's a version with some spurious data in the S (S p) case; I don't think the fix guardedness checker is looking at how many elements there are.

Inductive log_domain : nat -> Prop :=
  log_domain_1 : log_domain 1
| log_domain_2 : forall data p:nat, log_domain (S (Nat.div2 p)) -> log_domain (S (S p)).

Theorem log_domain_inv : forall x p:nat, log_domain x -> x = S (S p) -> log_domain (S (Nat.div2 p)).
Proof.
  intros x p H; case H; try (intros H'; discriminate H').
  intros _ p' H1 H2; injection H2; intros H3; rewrite <- H3; assumption.
Defined.

[Mario Carneiro]

This makes me wonder whether you can do recursion over acc in prop in rocq

[Mario Carneiro]

well this is fascinating:

Inductive acc {A: Type} (R: A -> A -> Prop): A -> Prop :=
  intro: forall x, (forall y, R y x -> acc R y) -> acc R x.

Theorem acc_inv {A: Type} {R: A -> A -> Prop} (x: A) (H: acc R x) : forall y, R y x -> acc R y.
Proof.
  intros y.
  case H.
  intros z H1 H2.
  exact (H1 _ H2).
Defined.

Fixpoint acc_rec {A: Type} {C: A -> Type} (R: A -> A -> Prop)
  (IH: forall x, (forall y, R y x -> C y) -> C x)
  (x: A) (H: acc R x): C x :=
IH x (fun y r => acc_rec R IH y (acc_inv _ H _ r)).

[Mario Carneiro]

and here's a "compilation to well founded recursion" of the previous example:

Inductive log_domain : nat -> Prop :=
  log_domain_1 : log_domain 1
| log_domain_2 : forall p:nat, log_domain (S (Nat.div2 p)) -> log_domain (S (S p)).

Inductive log_rel : nat -> nat -> Prop :=
  log_rel_2 : forall p:nat, log_rel (S (Nat.div2 p)) (S (S p)).

Theorem log_domain_acc : forall x:nat, log_domain x -> acc log_rel x.
Proof.
  intros x H. induction H; constructor; intros.
  * inversion H.
  * inversion H0; subst p0; assumption.
Qed.

Theorem log_domain_non_0 : forall x:nat, log_domain x -> x <> 0.
Proof.
  intros x H; case H; intros; discriminate.
Qed.

Theorem log_domain_inv : forall x p:nat, log_domain x -> x = S (S p) -> log_domain (S (Nat.div2 p)).
Proof.
  intros x p H. case H. try (intros H'; discriminate H').
  intros p' H1 H2. injection H2. intros H3. rewrite <- H3. assumption.
Qed.

Definition log (x:nat) (h:log_domain x) : nat :=
  acc_rec log_rel (fun x log h =>
    match x as y return x = y -> nat with
    | 0 => fun h' => False_rec nat (log_domain_non_0 x h h')
    | S 0 => fun h' => 0
    | S (S p) => fun h' =>
      S (log (S (Nat.div2 p)) ltac:(subst x; exact (log_rel_2 _)) (log_domain_inv x p h h'))
    end (refl_equal x)
  ) x (log_domain_acc x h) h.

[Mario Carneiro]

(note that log_domain_inv doesn't need to be unfoldable this time)

[Mario Carneiro]

the example is only as complicated as this because log_domain is also mixing in partiality (it's not defined at 0), while acc as written only handles well founded recursion without a domain restriction

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Are you claiming that recursion on Prop can always be reduced to one on Acc, so if I believe in the latter I must believe in the former?

[Kyod]

I think the puzzling thing with the two types

Inductive log_domain : nat -> Prop :=
  log_domain_1 : log_domain 1
| log_domain_2 : forall p:nat, log_domain (S (Nat.div2 p)) -> log_domain (S (S p)).

Inductive log_domain' : nat -> Prop :=
  log_domain_1' : log_domain' 1
| log_domain_2' : forall data p:nat, log_domain' (S (Nat.div2 p)) -> log_domain' (S (S p)).

is that they could be considered equivalent even though log_domain' looks like it contains more data. The point is that even though log_domain_2' has an additional argument data : nat, there is no way
1) to extract this argument in the Type world, and
2) no way to distinguish two nat within prop.

The first point would be a violation of the subsingleton elimination rule, and it is maybe easier to see that attempting to extract from a simpler inductive fails:

Inductive Sq : Prop := squash (data : nat) : Sq.

Goal Sq -> nat.
Proof.
  intros x.
 (* Annotating the pattern-matching for clarity *)
  refine (match x in Sq return nat with | squash n => n end).
  (* Error: *)
  (* Incorrect elimination of "x" in the inductive type "Sq": *)
  (* the return type has sort "Set" while it should be SProp or Prop. *)
  (* Elimination of an inductive object of sort Prop *)
  (* is not allowed on a predicate in sort "Set" *)
  (* because proofs can be eliminated only to build proofs. *)
Abort.

The second point correspond to the fact that you could extract the data component inside prop to a natProp proposition, but then you cannot tell zero and successor appart.

Inductive Sq : Prop := squash (data : nat) : Sq.

Inductive natProp : Prop := ZP : natProp | SP : natProp -> natProp.

Definition unsquash (x : Sq) : natProp :=
  match x with | squash n => nat_ind (fun _ => natProp) ZP (fun _ np => SP np) n end.

Goal ZP = SP ZP -> False.
  intros eq.
  discriminate eq.
  (* Error: Not a discriminable equality. *)

The two scripts I gave are only for illustration purpose, they do not prove that extraction from Sq to nat is impossible, nor that one cannot discriminate on natProp in Rocq, and it is not possible to show these properties within the system because they are only admissible consequences of the restriction of patter-matching on propositions to subsingletons.

Finally, I said that log_domain and log_domain' could be considered equivalent because you can build functions in both directions that will become equivalences under the assumption of (propositional) proof-irrelevance (cf def in stdlib; Prop and the subsingleton elimination constraints are designed to be compatible with this axiom)

Inductive log_domain : nat -> Prop :=
  log_domain_1 : log_domain 1
| log_domain_2 : forall p:nat, log_domain (S (Nat.div2 p)) -> log_domain (S (S p)).

Inductive log_domain' : nat -> Prop :=
  log_domain_1' : log_domain' 1
| log_domain_2' : forall data p:nat, log_domain' (S (Nat.div2 p)) -> log_domain' (S (S p)).

Fixpoint ll' {n} (x : log_domain n) : log_domain' n :=
  match x with
  | log_domain_1 => log_domain_1'
  | log_domain_2 p y => log_domain_2' 0 p (ll' y)
  end.

Fixpoint l'l {n} (x : log_domain' n) : log_domain n :=
  match x with
  | log_domain_1' => log_domain_1
  | log_domain_2' _ p y => log_domain_2 p (l'l y)
  end.

[Mario Carneiro]

While it's true that you can't directly eliminate Prop into Type, that's not sufficient to explain what's going on here. The point is that the guard checker has a rather different view of Prop which looks a whole lot more like Type even though the model of Prop is supposed to be consistent with a two element universe. In particular you can have a long sequence of "strictly smaller" terms inside a proof in Prop. There is no way to justify this from a two element Prop interpretation

[Mario Carneiro]

𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒 said:

Are you claiming that recursion on Prop can always be reduced to one on Acc, so if I believe in the latter I must believe in the former?

Yes, I believe Acc to be "universal" among large eliminating Prop inductives