Lean Prover Zulip Chat Archive

Stream: general

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


view this post on Zulip 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).

view this post on Zulip Mario Carneiro (Jul 24 2019 at 09:03):

Yes, lean cares about the order of arguments here

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jul 24 2019 at 09:05):

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

view this post on Zulip 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 :-/

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jul 24 2019 at 09:10):

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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Jul 24 2019 at 09:16):

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

view this post on Zulip Mario Carneiro (Jul 24 2019 at 09:16):

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

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jul 24 2019 at 09:19):

Inductive predicates are also fairly common

view this post on Zulip Cyril Cohen (Jul 24 2019 at 09:21):

Inductive predicates are also fairly common

could you give me examples?

view this post on Zulip Mario Carneiro (Jul 24 2019 at 09:26):

The inductive predicate in_closure s a defines the subgroup closure

view this post on Zulip Mario Carneiro (Jul 24 2019 at 09:28):

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

view this post on Zulip 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 :(

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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:

view this post on Zulip 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

view this post on Zulip Cyril Cohen (Jul 24 2019 at 09:42):

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

view this post on Zulip 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]

view this post on Zulip 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

view this post on Zulip Cyril Cohen (Jul 24 2019 at 09:44):

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

view this post on Zulip Mario Carneiro (Jul 24 2019 at 09:44):

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

view this post on Zulip 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!

view this post on Zulip Mario Carneiro (Jul 24 2019 at 09:47):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jul 24 2019 at 09:50):

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

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip Mario Carneiro (Jul 24 2019 at 09:53):

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

view this post on Zulip Mario Carneiro (Jul 24 2019 at 09:53):

feel free to ignore my ramblings

view this post on Zulip Cyril Cohen (Jul 24 2019 at 09:53):

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

Would you have examples in mind?

view this post on Zulip Mario Carneiro (Jul 24 2019 at 09:53):

Stuff like rw will not like if you wrap a constructor

view this post on Zulip 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...

view this post on Zulip Cyril Cohen (Jul 24 2019 at 09:54):

Stuff like rw will not like if you wrap a constructor

What specific use or rw?

view this post on Zulip Mario Carneiro (Jul 24 2019 at 09:54):

Also you can't pattern match on a wrapped constructor

view this post on Zulip Mario Carneiro (Jul 24 2019 at 09:54):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jul 24 2019 at 09:56):

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

view this post on Zulip Mario Carneiro (Jul 24 2019 at 09:57):

What does the parametricity translation do to choice?

view this post on Zulip 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 ^^'

view this post on Zulip Cyril Cohen (Jul 24 2019 at 10:07):

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

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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 ;)

view this post on Zulip 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!

view this post on Zulip 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 :-/

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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:

view this post on Zulip 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