Induction over inductive families

Stream: new members

[Devon Tuma]

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]

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]

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

[Mario Carneiro]

what happened to that eq_dec argument in your lean version?

[Devon Tuma]

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]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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]

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]

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

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

[Devon Tuma]

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]

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]

Surely this type doesn't have decidable equality though?

[Reid Barton]

Since there's a function in the Bind constructor

[Mario Carneiro]

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]

but it still wouldn't be decidable

[Devon Tuma]

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]

Apologies for the confusion

[Mario Carneiro]

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