## Stream: general

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

#### Cyril Cohen (Jul 24 2019 at 08:54):

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 vhd1 vtl1) (rvcons vhd1 vtl1).


#### Mario Carneiro (Jul 24 2019 at 09:03):

Yes, lean cares about the order of arguments here

#### Mario Carneiro (Jul 24 2019 at 09:04):

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 (Jul 24 2019 at 09:05):

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

#### Cyril Cohen (Jul 24 2019 at 09:07):

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 (Jul 24 2019 at 09:09):

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 (Jul 24 2019 at 09:10):

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 (Jul 24 2019 at 09:10):

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

#### Cyril Cohen (Jul 24 2019 at 09:15):

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 (Jul 24 2019 at 09:16):

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

#### Mario Carneiro (Jul 24 2019 at 09:16):

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

#### Mario Carneiro (Jul 24 2019 at 09:17):

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 (Jul 24 2019 at 09:17):

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 (Jul 24 2019 at 09:17):

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 (Jul 24 2019 at 09:19):

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 (Jul 24 2019 at 09:19):

Inductive predicates are also fairly common

#### Cyril Cohen (Jul 24 2019 at 09:21):

Inductive predicates are also fairly common

could you give me examples?

#### Mario Carneiro (Jul 24 2019 at 09:26):

The inductive predicate in_closure s a defines the subgroup closure

#### Mario Carneiro (Jul 24 2019 at 09:28):

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

#### Cyril Cohen (Jul 24 2019 at 09:29):

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 (Jul 24 2019 at 09:31):

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 (Jul 24 2019 at 09:33):

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 (Jul 24 2019 at 09:41):

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 (Jul 24 2019 at 09:42):

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 (Jul 24 2019 at 09:42):

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

#### Mario Carneiro (Jul 24 2019 at 09:43):

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

#### Cyril Cohen (Jul 24 2019 at 09:43):

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 (Jul 24 2019 at 09:44):

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

#### Mario Carneiro (Jul 24 2019 at 09:44):

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

#### Cyril Cohen (Jul 24 2019 at 09:46):

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 (Jul 24 2019 at 09:47):

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

#### Mario Carneiro (Jul 24 2019 at 09:48):

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

#### Cyril Cohen (Jul 24 2019 at 09:48):

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 (Jul 24 2019 at 09:50):

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

#### Mario Carneiro (Jul 24 2019 at 09:51):

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 (Jul 24 2019 at 09:52):

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 (Jul 24 2019 at 09:53):

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

#### Mario Carneiro (Jul 24 2019 at 09:53):

feel free to ignore my ramblings

#### Cyril Cohen (Jul 24 2019 at 09:53):

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

Would you have examples in mind?

#### Mario Carneiro (Jul 24 2019 at 09:53):

Stuff like rw will not like if you wrap a constructor

#### Cyril Cohen (Jul 24 2019 at 09:54):

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 (Jul 24 2019 at 09:54):

Stuff like rw will not like if you wrap a constructor

What specific use or rw?

#### Mario Carneiro (Jul 24 2019 at 09:54):

Also you can't pattern match on a wrapped constructor

#### Mario Carneiro (Jul 24 2019 at 09:54):

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

#### Mario Carneiro (Jul 24 2019 at 09:55):

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 (Jul 24 2019 at 09:55):

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 (Jul 24 2019 at 09:56):

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

#### Mario Carneiro (Jul 24 2019 at 09:57):

What does the parametricity translation do to choice?

#### Cyril Cohen (Jul 24 2019 at 10:06):

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 (Jul 24 2019 at 10:07):

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

#### Johan Commelin (Jul 24 2019 at 10:13):

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 (Jul 24 2019 at 10:14):

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

#### Mario Carneiro (Jul 24 2019 at 10:24):

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

#### Mario Carneiro (Jul 24 2019 at 10:25):

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

#### Mario Carneiro (Jul 24 2019 at 10:38):

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 (Jul 24 2019 at 11:14):

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 (Jul 24 2019 at 11:16):

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

#### Cyril Cohen (Jul 24 2019 at 11:21):

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

#### Cyril Cohen (Jul 24 2019 at 11:22):

@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 property statements (opaque/proof-irrelevant non constructive proofs are okay, I would say)

#### Cyril Cohen (Jul 24 2019 at 11:52):

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 (Jul 24 2019 at 12:05):

@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 (Jul 24 2019 at 12:17):

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 (Jul 24 2019 at 12:22):

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 (Jul 24 2019 at 12:23):

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

#### Mario Carneiro (Jul 24 2019 at 12:33):

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


Last updated: Nov 12 2019 at 10:00 UTC