invalid occurrence of recursive arg#10 of 'rvec.param.vcons'

Stream: general

[Cyril Cohen]

The following code leads to the error message invalid occurrence of recursive arg#10 of 'rvec.param.vcons', the body of the functional type depends on it.

Lean seems to care about where the argument vhdR (of the cons constructor of my rvec.param inductive type) is located. I do not understand from where this restriction comes... @Mario Carneiro @Johannes Hölzl @Rob Lewis an idea about that? I am particularily surprised because the Coq equivalent works (see snippet below)

Lean code:

universe u

inductive rvec (α : Sort u) : ℕ → Type u
| nil {} : rvec nat.zero
| cons {n : ℕ} (vhd : rvec n) (vtl : α) : rvec n.succ

inductive nat.param : ℕ → ℕ → Type
| zero : nat.param 0 0
| succ : Π (n0 n1 : ℕ), nat.param n0 n1 → nat.param (nat.succ n0) (nat.succ n1)

inductive rvec.param (α0 : Sort.{u}) (α1 : Sort.{u}) (αR : α0 -> α1 -> Sort.{u}) :
  Π (a0 : nat) (a1 : nat) (aR : nat.param a0 a1) (x0 : rvec.{u} α0 a0) (x1 : rvec.{u} α1 a1), Type.{u}
| nil : rvec.param nat.zero nat.zero nat.param.zero (rvec.nil.{u}) (rvec.nil.{u})
| cons (n0 : nat) (n1 : nat) (nR : nat.param n0 n1)
    (vhd0 : rvec.{u} α0 n0) (vhd1 : rvec.{u} α1 n1)
    (vhdR : rvec.param n0 n1 nR vhd0 vhd1) /- this must be after vtl1, but why? -/
    (vtl0 : α0) (vtl1 : α1) (vtlR : αR vtl0 vtl1)
    :
  rvec.param (nat.succ n0) (nat.succ n1) (nat.param.succ n0 n1 nR)
    (rvec.cons.{u} vhd0 vtl0) (rvec.cons.{u} vhd1 vtl1)

Coq code:

Set Implicit Arguments.

Inductive rvec A : nat -> Type :=
| rvnil : rvec A 0
| rvcons {n : nat} (vhd : rvec A n) (vtl : A) : rvec A (S n).

Inductive natR : nat -> nat -> Set :=
| OR : natR 0 0
| SR : forall n0 n1 : nat, natR n0 n1 -> natR (S n0) (S n1).

Inductive rvecR (A0 A1 : Type) (AR : A0 -> A1 -> Type) :
    forall n0 n1 : nat, natR n0 n1 -> rvec A0 n0 -> rvec A1 n1 -> Type :=
| rvnilR : rvecR AR OR (rvnil A0) (rvnil A1)
| rvconsR : forall (n0 n1 : nat) (nR : natR n0 n1)
      (vhd0 : rvec A0 n0) (vhd1 : rvec A1 n1), rvecR AR nR vhd0 vhd1 ->
      forall (vtl0 : A0) (vtl1 : A1), AR vtl0 vtl1 ->
    rvecR AR (SR nR) (rvcons vhd0 vtl0) (rvcons vhd1 vtl1).

[Mario Carneiro]

Yes, lean cares about the order of arguments here

[Mario Carneiro]

It's an arbitrary restriction, but it makes things easier since otherwise you have to worry about the vhd argument appearing somewhere weird in wtl

[Mario Carneiro]

It obviously makes no mathematical difference, as you can just reorder the arguments

[Cyril Cohen]

It obviously makes no mathematical difference, as you can just reorder the arguments

Since I am meta-programming a parametricity transformation, "reordering arguments" introduces the need to make additional wrappers here and there :-/

[Cyril Cohen]

It's an arbitrary restriction, but it makes things easier since otherwise you have to worry about the vhd argument appearing somewhere weird in wtl

I still do not understand why it is working for rvec and not for rvec.param though...

[Mario Carneiro]

Actually my judgment was premature. This used to not even be allowed in rvec, but the restriction was lifted at some point, apparently not enough

[Mario Carneiro]

I think the difference is that vtl0 and vtl1 appear in parameters in the return type

[Cyril Cohen]

OK, then do you think I can safely ignore types such as rvec during my translation, for such types will not be in lean core or in mathlib?

[Mario Carneiro]

What do you mean? What is the goal, are you translating Coq proofs to lean?

[Mario Carneiro]

It is certainly true that rvec won't be in mathlib

[Mario Carneiro]

Actually mathlib is pretty sparse on fancy inductive types, because mathematicians rule the roost around here and they don't see the point

[Cyril Cohen]

What do you mean? What is the goal, are you translating Coq proofs to lean?

no, I am writing a parametricity translation for lean, which might be run on any inductive type in existing libraries. So I am wondering if there will be real cases where the recursive argument of a constructor does not come last...

[Cyril Cohen]

Actually mathlib is pretty sparse on fancy inductive types, because mathematicians rule the roost around here and they don't see the point

Then I am lucky :D

[Mario Carneiro]

I'm honestly drawing a blank on any inductive types other than really basic stuff like sum and sigma that are already defined in core. It's all structures

[Mario Carneiro]

Inductive predicates are also fairly common

[Cyril Cohen]

Inductive predicates are also fairly common

could you give me examples?

[Mario Carneiro]

The inductive predicate in_closure s a defines the subgroup closure

[Mario Carneiro]

https://github.com/leanprover-community/mathlib/blob/master/src/group_theory/subgroup.lean#L468-L472

[Cyril Cohen]

https://github.com/leanprover-community/mathlib/blob/master/src/group_theory/subgroup.lean#L468-L472

damn, I am probably going to run into trouble because of this one :(

[Mario Carneiro]

Here's another example of a not completely trivial inductive predicate
https://github.com/leanprover-community/mathlib/blob/master/src/data/list/defs.lean#L379-L381

[Cyril Cohen]

Here's another example of a not completely trivial inductive predicate
https://github.com/leanprover-community/mathlib/blob/master/src/data/list/defs.lean#L379-L381

this one looks less problematic to me because the recursive argument comes last and only once. (parametricity introduces duplications and interleaving which causes the problem)

[Cyril Cohen]

https://github.com/leanprover-community/mathlib/blob/master/src/group_theory/subgroup.lean#L468-L472

damn, I am probably going to run into trouble because of this one :(

Indeed...

inductive in_closure (α : Type u) : α → Prop
| basic (a : α) : in_closure a
| mul {a : α} : in_closure a → in_closure a → in_closure a

inductive in_closure.param (α0 : Type) (α1 : Type) (αR : α0 -> α1 -> Type) :
 Π (a0 : α0) (a1 : α1) (aR : αR a0 a1)
   (x0 : in_closure α0 a0) (x1 : in_closure α1 a1), Prop
| basic (a0 : α0) (a1 : α1) (aR : αR a0 a1) :
  (in_closure.param a0 a1 aR (in_closure.basic a0)
   (in_closure.basic a1))
| mul (a0 : α0) (a1 : α1) (aR : αR a0 a1)
      (a0_1 : in_closure α0 a0) (a1_1 : in_closure α1 a1)
      (aR_1 : in_closure.param a0 a1 aR a0_1 a1_1)
      (a0_2 : in_closure α0 a0) (a1_2 : in_closure α1 a1)
      (aR_1 : in_closure.param a0 a1 aR a0_2 a1_2) :
      (in_closure.param a0 a1 aR
      (in_closure.mul a0_1 a0_2) (in_closure.mul a1_1 a1_2))

does not go through... :dizzy:

[Mario Carneiro]

Yeah, I think I see how the algorithm goes and you will only be able to handle one recursive arg which comes last

[Cyril Cohen]

so I will have to perform reordering and wrap things around...

[Mario Carneiro]

But you should be able to order the arguments as [a0, a1, b0, b1, c0, c1, aR, bR, cR]

[Cyril Cohen]

But you should be able to order the arguments as [a0, a1, b0, b1, c0, c1, aR, bR, cR]

Yes, that is what I will do, but since it is not the "canonical" order, I will have to do wrappers

[Cyril Cohen]

Actually I am going to do [a0, b0, c0, a1, b1, c1, aR, bR, cR]

[Mario Carneiro]

or remember that this is a "funny order definition" and apply the reordering in the theorems

[Cyril Cohen]

or remember that this is a "funny order definition" and apply the reordering in the theorems

my intuition whispers to me is that it is better to precompute the reordering as wrappers rather than on each application. Thanks for your time and advice!

[Mario Carneiro]

You will need the wrappers to be pretty transparent lest they break defeq stuff

[Mario Carneiro]

Presumably you aren't writing tactic scripts with the metaprogramming so it may not be a big deal

[Cyril Cohen]

You will need the wrappers to be pretty transparent lest they break defeq stuff

I'm not sure I understand, but I don't think they should be transparent

[Mario Carneiro]

wrappers have a tendency to change inference and break tactics that look at the expression

[Mario Carneiro]

for pure proof terms you can get away with defeq but most of the time it matters when you have a constructor vs a definition that unfolds to a constructor

[Cyril Cohen]

for pure proof terms you can get away with defeq but most of the time it matters when you have a constructor vs a definition that unfolds to a constructor

I do not understand how a definition that unfolds to a constructor can break defeq...

[Mario Carneiro]

It won't break defeq, it will break other things

[Mario Carneiro]

feel free to ignore my ramblings

[Cyril Cohen]

It won't break defeq, it will break other things

Would you have examples in mind?

[Mario Carneiro]

Stuff like rw will not like if you wrap a constructor

[Cyril Cohen]

feel free to ignore my ramblings

I'd rather not ignore them! I'd like to be aware if I will break something unintentionally...

[Cyril Cohen]

Stuff like rw will not like if you wrap a constructor

What specific use or rw?

[Mario Carneiro]

Also you can't pattern match on a wrapped constructor

[Mario Carneiro]

and cases and the inductive recursor will not re-wrap the constructor for you

[Mario Carneiro]

there was a thread here last week about making proofs by induction show 0 in the base case instead of my_nat.zero

[Cyril Cohen]

I think rw and pattern matching are not a concern since the purpose of parametricity translations is mostly for automations... but I need to think twice

[Mario Carneiro]

Like I said, carry on, you probably don't have to worry

[Mario Carneiro]

What does the parametricity translation do to choice?

[Cyril Cohen]

What does the parametricity translation do to choice?

Since Pierce law is provably non parametric, so are LEM and any choice axiom that would entail it, ... so I will probably send an error message... (the error message will read: "cannot transfer your theorems because you were not constructive enough").
This will be an incentive to write constructive functions and structures, since otherwise transfer by isomorphism theorems will not work ^^'

[Cyril Cohen]

(And maybe mathematicians will finally see the point in constructive maths :P)

[Johan Commelin]

I'm afraid that we will just complain that we want better transfer. Because in real world maths we can easily transport non-constructive properties/functions/data/etc...

[Johan Commelin]

Which is not meant as discouragement to you. Because I think any improvement of the transfer ecosystem is already a big win.

[Mario Carneiro]

I think that this is a more important point than transferring weird inductive types. Large swaths of mathlib are nonconstructive

[Mario Carneiro]

But more precisely, can you say what would happen if you apply the parametricity transformation to choice?

[Mario Carneiro]

I don't think I did this right...

inductive nonempty.param
  (α0 α1 : Sort u) (αR : α0 → α1 → Sort u) :
  nonempty α0 → nonempty α1 → Prop
| intro (a0 : α0) (a1 : α1) (aR : αR a0 a1) :
  nonempty.param (nonempty.intro a0) (nonempty.intro a1)

axiom choice.param
  (α0 α1 : Sort u) (αR : α0 → α1 → Sort u)
  (h0 : nonempty α0) (h1 : nonempty α1) (hR : nonempty.param α0 α1 αR h0 h1) :
  α0 → α1 → Prop

[Cyril Cohen]

I don't think I did this right...

inductive nonempty.param
  (α0 α1 : Sort u) (αR : α0 → α1 → Sort u) :
  nonempty α0 → nonempty α1 → Prop
| intro (a0 : α0) (a1 : α1) (aR : αR a0 a1) :
  nonempty.param (nonempty.intro a0) (nonempty.intro a1)

axiom choice.param
  (α0 α1 : Sort u) (αR : α0 → α1 → Sort u)
  (h0 : nonempty α0) (h1 : nonempty α1) (hR : nonempty.param α0 α1 αR h0 h1) :
  α0 → α1 → Prop

inductive nonempty.param : Π (α0 α1 : Sort u), (α0 → α1 → Sort u) → nonempty α0 → nonempty α1 → Prop
| intro (α0 α1 : Sort u) (αR : α0 → α1 → Sort u) (val0 : α0) (val1 : α1) : αR val0 val1 →
          nonempty.param α0 α1 αR (nonempty.intro val0) (nonempty.intro val1)

axiom choice.param (α0 α1 : Sort u) (αR : α0 → α1 → Sort u) (a0 : nonempty α0) (a1 : nonempty α1) :
    nonempty.param α0 α1 αR a0 a1 → αR (classical.choice a0) (classical.choice a1)

I am cheating, my plugin is already able to perform these transformations ;)

[Cyril Cohen]

I was sure one can derive false from choice.param, but I cannot find the reference anymore, so maybe I'm wrong!

[Cyril Cohen]

https://arxiv.org/pdf/1209.6336.pdf 5.4.2 but they do not reference the proof :-/

[Cyril Cohen]

@Johan Commelin

I'm afraid that we will just complain that we want better transfer. Because in real world maths we can easily transport non-constructive properties/functions/data/etc...

I'm afraid I do not know any consistent logical foundation for transporting non constructive functions or proof of constructive statements (opaque/proof-irrelevant non constructive proofs are okay, I would say)

[Cyril Cohen]

Here is the proof that em.param is false.

inductive or.param : Π (a0 a1 : Prop), (a0 → a1 → Prop) →
  Π (b0 b1 : Prop), (b0 → b1 → Prop) → a0 ∨ b0 → a1 ∨ b1 → Prop
| inl : ∀ (a0 a1 : Prop) (aR : a0 → a1 → Prop) (b0 b1 : Prop) (bR : b0 → b1 → Prop) (h0 : a0) (h1 : a1),
  aR h0 h1 → or.param a0 a1 aR b0 b1 bR (or.inl h0) (or.inl h1)
| inr : ∀ (a0 a1 : Prop) (aR : a0 → a1 → Prop) (b0 b1 : Prop) (bR : b0 → b1 → Prop) (h0 : b0) (h1 : b1),
  bR h0 h1 → or.param a0 a1 aR b0 b1 bR (or.inr h0) (or.inr h1)

inductive false.param : false → false → Prop

def not.param : Π (a0 a1 : Prop), (a0 → a1 → Prop) → ¬a0 → ¬a1 → Prop :=
λ (a0 a1 : Prop) (aR : a0 → a1 → Prop) (f0 : a0 → false) (f1 : a1 → false),
  ∀ (a0 : a0) (a1 : a1), aR a0 a1 → false.param (f0 a0) (f1 a1)

axiom em.param : ∀ (p0 p1 : Prop) (pR : p0 → p1 → Prop),
  or.param p0 p1 pR (¬p0) (¬p1) (not.param p0 p1 pR) (classical.em p0) (classical.em p1)

lemma em_param_is_false : false := begin
  cases em.param true false (λ _ _, true), {exact h1}, {apply h0, exact true.intro}
end

[Cyril Cohen]

@Mario Carneiro

I think that this is a more important point than transferring weird inductive types. Large swaths of mathlib are nonconstructive

I think the opposite: most of the statements are stated without classical features, but I should be able to translate any such statement, even if it contains a weird inductive predicate.

[Mario Carneiro]

I think it is important to be able to translate classical results that depend on other definitions that are classical but can be proven to be parametric by other means

[Cyril Cohen]

I think it is important to be able to translate classical results that depend on other definitions that are classical but can be proven to be parametric by other means

Of course! but then you provide the parametricity proofs you depend on by hand. Most transfer result will be parametrized by isomorphisms anyway (which are special cases of parametricity relations).

[Cyril Cohen]

Most of the time, the simplest way to prove something parametric will still be to give a constructive alternative definition :joy:

[Mario Carneiro]

inductive nonempty.param
  (α0 α1 : Sort u) (αR : α0 → α1 → Prop) :
  nonempty α0 → nonempty α1 → Prop
| intro (a0 : α0) (a1 : α1) (aR : αR a0 a1) :
  nonempty.param (nonempty.intro a0) (nonempty.intro a1)

axiom choice.param (α0 α1 : Sort u) (αR : α0 → α1 → Prop)
  (a0 : nonempty α0) (a1 : nonempty α1) : nonempty.param α0 α1 αR a0 a1 →
  αR (classical.choice a0) (classical.choice a1)

example : false :=
let R := nonempty.param bool bool (≠) in
choice.param _ _ _ _ _ (⟨ff, tt, bool.ff_ne_tt⟩ : R ⟨ff⟩ ⟨tt⟩) rfl