## Stream: new members

### Topic: Induction over inductive families

#### Devon Tuma (Jan 29 2021 at 20:26):

I've been trying to adapt some proofs written in Coq, and I'm having trouble proving decidable equality on an inductive family of types. A simplified version of the problem looks like this:

import data.bitvec.basic

set_option trace.check true

inductive C : Type* → Sort*
| Foo : Π {A : Type*} (a : A), C A
| Bar : Π (n : ℕ), C (bitvec n)

open C

example {A : Type*} [hA : decidable_eq A] : decidable_eq (C A) :=
λ c1 c2,
begin
tactic.unfreeze_local_instances,
induction c1 with A a n generalizing c2,
{ cases c2 with A a',
{ cases hA a a',
{ refine is_false (mt Foo.inj h) },
{ refine is_true (congr_arg Foo h) } },
{ refine is_false (by contradiction) } },
{
sorry
},
end


induction and cases fail because of motive issues with the differing lengths of the bitvectors, and I can't make the proof go through with the recursors either. Is there a better way to handle this kind of nested induction? Or have I defined the inductive family badly in some way?

#### Devon Tuma (Jan 29 2021 at 20:28):

For reference, the family in Coq looks something like:

Inductive C: Set -> Type :=
| Foo: forall (A : Set), eq_dec A -> A -> C A
| Bar: forall n, C (Bvector n)


#### Mario Carneiro (Jan 29 2021 at 20:31):

That's a bit different, isn't it?

#### Mario Carneiro (Jan 29 2021 at 20:31):

what happened to that eq_dec argument in your lean version?

#### Devon Tuma (Jan 29 2021 at 20:33):

I tried moving it between the constructor and lemma hypothesis to see if that would help with the problem, but either way I couldn't get the proofs to work

#### Devon Tuma (Jan 29 2021 at 20:33):

It seemed mostly orthogonal to the induction/recursor problems I was having, but I could be wrong about that

#### Mario Carneiro (Jan 29 2021 at 20:50):

This theorem is true but nontrivially so:

instance (n) : fintype (bitvec n) := sorry
theorem bitvec.card (n) : fintype.card (bitvec n) = 2 ^ n := sorry

example {A : Type*} [hA : decidable_eq A] : decidable_eq (C A) :=
λ c1 c2,
begin
tactic.unfreeze_local_instances,
suffices : ∀ A' (e : A = A') (c2 : C A'), decidable (c1 == c2),
{ exact decidable_of_decidable_of_iff (this _ rfl _) heq_iff_eq },
clear c2, intros,
cases c1 with A a n,
{ subst e, cases c2 with A a',
{ exact decidable_of_iff (a = a') (by simp) },
{ apply is_false, rw heq_iff_eq, contradiction } },
{ cases c2 with A a' m,
{ apply is_false, cases e, rw heq_iff_eq, contradiction },
{ apply is_true,
congr,
have : fintype.card (bitvec n) = fintype.card (bitvec m), {congr'},
rw [bitvec.card, bitvec.card] at this,
exact nat.pow_right_injective dec_trivial this } },
end


#### Mario Carneiro (Jan 29 2021 at 20:51):

For the most part type constructors are not injective, and you need that in order for this theorem to be true

#### Mario Carneiro (Jan 29 2021 at 20:51):

in this case you picked bitvec, which is injective, because it's a finite type whose size is an injective function of the input

#### Mario Carneiro (Jan 29 2021 at 20:54):

This is a really weird inductive type though. If I could #xy the problem, what do you need this type for?

#### Mario Carneiro (Jan 29 2021 at 20:56):

Generally speaking type equalities are a bad idea and this type is basically saying that C A is A unless A = bitvec n in which case it is option A

#### Mario Carneiro (Jan 29 2021 at 20:56):

which makes it more or less useless for other types like say fin 2 because you don't know whether or not fin 2 = bitvec 1 is true

#### Mario Carneiro (Jan 29 2021 at 20:58):

that is, this proposition is independent of lean's axioms

#check ∀ x : C (fin 2), ∃ a, x = Foo a


#### Devon Tuma (Jan 29 2021 at 21:04):

The full original Coq definition looks like this:

Inductive Comp : Set -> Type :=
| Ret : forall (A : Set), eq_dec A -> A -> Comp A
| Bind : forall (A B : Set), Comp B -> (B -> Comp A) -> Comp A
| Rnd : forall n, Comp (Bvector n)
| Repeat : forall (A : Set), Comp A -> (A -> bool) -> Comp A.


And is meant to be a shallow embedding of a basic programming language (where the Rnd constructor is a computation of some random bits for cryptography purposes). I was curious to see if something like this would work in Lean, but ran into the above issue.

#### Devon Tuma (Jan 29 2021 at 21:11):

In general then is it a bad idea to have some type constructors of the family produce more generic types than other constructors? So it would be better to have some kind of rnd_gen A Prop for types that can be randomly generated, and then have Rnd look like Rnd : forall {A : Type*}, rnd_gen A -> Comp A?

#### Reid Barton (Jan 29 2021 at 21:21):

Surely this type doesn't have decidable equality though?

#### Reid Barton (Jan 29 2021 at 21:22):

Since there's a function in the Bind constructor

#### Mario Carneiro (Jan 29 2021 at 21:24):

Yeah, I don't see the value in attempting to prove decidable equality for this type. Seems like it would be more useful, if you cared about equality on this type, to at least quotient by the monad laws

#### Mario Carneiro (Jan 29 2021 at 21:25):

but it still wouldn't be decidable

#### Devon Tuma (Jan 29 2021 at 21:34):

Going back to the orignal paper, it seems like I majorly tunnel-visioned on what the actual claim was. The statement shouldn't be decidable_eq A -> decidable_eq (Comp A), instead it should be Comp A -> decidable_eq A, which is a much more reasonable statement to prove. Seems like I was so used to Lean naming conventions that I just assumed the content of the lemma based on its name

#### Devon Tuma (Jan 29 2021 at 21:34):

Apologies for the confusion

#### Mario Carneiro (Jan 29 2021 at 21:54):

Of course you need the decidable_eq assumption inside the type for that to be true

Last updated: May 12 2021 at 23:13 UTC