induction for custom dependent type

Stream: lean4

[Abdullah Al Kayal]

I have defined an inductive type called Circuit with the following implementation:

inductive Circuit : Nat → Type
| wire : Circuit 1
| empty : Circuit 0
| tof : Circuit 3
| swap {n : Nat} (f1 : Fin n) (f2 : Fin n) : Circuit n
| comp {n : Nat} (c1 : Circuit n) (c2 : Circuit n) : Circuit n
| tensorProduct {n m : Nat} (c1 : Circuit n) (c2 : Circuit m) : Circuit (n + m)

notation "∅" => empty

I am trying to prove the following theorem:

theorem circ_zero_empty (c : Circuit 0) : c = ∅ :=
by
  cases c
  ...

There are three problems with this:

1. When I apply the cases tactic on c, I only get the empty, swap and comp cases, but I don't get the tensorProduct one.
2. I am trying to use induction instead of cases, as I don't know how to prove the comp or tensorProduct cases without an induction hypothesis, but when I try to do so, I get the following error:

index in target's type is not a variable (consider using the `cases` tactic instead)
  0

I understand that c has type Circuit 0 and not Circuit n but I don't understand why this would make induction not applicable to it.

3. Even when I try to prove the trivial case ∅ = ∅, I get the following error:

theorem circ_zero_empty (c : Circuit 0) : c = ∅ :=
by
  cases c with
  | empty =>
    rfl
    /-
    dependent elimination failed, failed to solve equation
    0 = n✝.add m✝
    -/

[Aaron Liu]

cases doesn't give you the tensorProduct case because it doesn't know if 0 = n + m is a valid combination. induction isn't smart enough yet to figure out how to do induction on Circuit 0, it only knows how to do Circuit n.
You can turn Circuit 0 into Circuit n with generalize h : 0 = n at c, and you get c : Circuit n and h : n = 0. Then, you can do induction c to induct on c.

[Aaron Liu]

See #new members > Type mismatch when matching inductive dependent type

[Edward van de Meent]

alternatively, it might be easier to work with a version of the type where there is no natural number in the type, and rather define a degree or rank (or whatever it's called) function Circuit -> Nat

[Abdullah Al Kayal]

@Aaron Liu are you telling me to use recursion instead of induction. I've seen this page that explains it, but how can I use it in this case?

[Abdullah Al Kayal]

@Edward van de Meent do you mean define it in a similar fashion to e.g. List.Vector?

[Edward van de Meent]

yes, something like this:

set_option autoImplicit false

inductive Circuit' : Type
| wire : Circuit'
| empty : Circuit'
| tof : Circuit'
| swap {n : Nat} (f1 : Fin n) (f2 : Fin n) : Circuit'
| comp (c1 : Circuit') (c2 : Circuit') : Circuit'
| tensorProduct (c1 : Circuit') (c2 : Circuit') : Circuit'

def Circuit'.degree (c:Circuit') : Nat := match c with
  | .wire => 1
  | .empty => 0
  | .tof => 3
  | @swap n _ _ => n
  | .comp l r => max l.degree r.degree
  | .tensorProduct l r => l.degree + r.degree

/-- a `Circuit'` is well-formed when every constituent `comp` constructor uses degrees of the right size. -/
inductive Circuit'.wf : Circuit' → Prop
  | isWire : wire.wf
  | isEmpty : empty.wf
  | isTof : tof.wf
  | isSwap {n} (f1 f2 : Fin n) : (swap f1 f2).wf
  | isComp {l r : Circuit'} (hl : l.wf) (hr : r.wf) (heq : l.degree = r.degree) : (comp l r).wf
  | isTensorProduct {l r : Circuit'} (hl : l.wf) (hr : r.wf): (tensorProduct l r).wf

def Circuit (n:Nat) : Type := {c:Circuit' // c.wf ∧ c.degree = n}

[Edward van de Meent]

ah, i just realised this will not actually help you prove the theorem you're trying to prove, since .comp .empty .empty will still be different from .empty

[Aaron Liu]

This is suspicious

theorem not_circ_zero_empty : ¬∀ (c : Circuit 0), c = ∅ := by
  intro h
  specialize h (.comp ∅ ∅)
  simp at h

[Edward van de Meent]

well, that's just how the defined type works... perhaps it might be useful if you would give a reference as to what is being modeled (or rather, what this is supposed to model)

[Abdullah Al Kayal]

Aaron Liu said:

This is suspicious

theorem not_circ_zero_empty : ¬∀ (c : Circuit 0), c = ∅ := by
  intro h
  specialize h (.comp ∅ ∅)
  simp at h

That confused me even more :smiling_face_with_tear: . Does that then imply that what I'm trying to prove is wrong in the first place. But then I don't really understand why it would be.

My goal state after specialize h (.comp ∅ ∅)is

h : (∅∘∅) = ∅
⊢ False

Does that imply that (∅∘∅) = ∅ is a contradiction?

[Aaron Liu]

Yes

[Abdullah Al Kayal]

But why.

[Aaron Liu]

You have comp _ _ = empty

[Edward van de Meent]

because by definition of inductive types, the things you construct with .comp are different from those you construct with .empty

[Abdullah Al Kayal]

oh is that it

[Aaron Liu]

Because you can distinguish comp from empty by pattern matching, so they can't be the same

[Abdullah Al Kayal]

Is there some way around it (besides defining it like @Edward van de Meent suggested)?

[Edward van de Meent]

my suggestion doesn't fix this, unfortunately

[Edward van de Meent]

what are you trying to model with the Circuit type? is there some literature you're following?

[Abdullah Al Kayal]

There isn't really any literature that I'm closely following, I am just trying to define the set of reversable computations using this Circuit definition.

[Abdullah Al Kayal]

Anyway thank you guys, I guess I'll have to rework on my definitions then.

[Edward van de Meent]

thinking about it, there might be a way to do this... if there is such a thing as a normal form of these circuits, you can create a predicate saying an element of Circuit' is in normal form, then add that to the required proofs for Circuit

[Aaron Liu]

You could define a predicate relation saying that two circuits are "the same", and quotient by that predicate relation.

[Edward van de Meent]

(quotients are worse to work with than subtypes, fyi)

[Edward van de Meent]

ah, i think i finally know what you're trying to model:

structure Circuit where
  size : Nat
  -- equiv : Fin size ≃ Fin size -- use this rather than the following when using mathlib
  toFun : Fin size → Fin size
  invFun : Fin size → Fin size
  left_inv : ∀ (i : Fin size), toFun (invFun i) = i
  right_inv : ∀ (i : Fin size), invFun (toFun i) = i

you don't get induction automatically this way, however

[Aaron Liu]

what is tof : Circuit 3

[Aaron Liu]

My guess is some kind of junction

[Edward van de Meent]

true or false?

[Edward van de Meent]

:thinking: but then my model is still missing something

[Edward van de Meent]

i'm guessing it's a trinary operator (with 3 resulting arguments) which swaps b and c depending on if a is true or not

[Edward van de Meent]

so then, a maybe more accurate representation would be this:

structure Circuit where
  size : Nat
  -- equiv : (Fin size → Bool) ≃ (Fin size → Bool) -- use this rather than the following when using mathlib
  toFun : (Fin size → Bool) → (Fin size → Bool)
  invFun : (Fin size → Bool) → (Fin size → Bool)
  left_inv : ∀ (v : Fin size → Bool), toFun (invFun v) = v
  right_inv : ∀ (v : Fin size → Bool), invFun (toFun v) = v

[Kyle Miller]

I don't see another trick mentioned, which is to embed the equality in the type, saving you from needing to generalize:

inductive Circuit : Nat → Type
| wire : Circuit 1
| empty : Circuit 0
| tof : Circuit 3
| swap {n : Nat} (f1 : Fin n) (f2 : Fin n) : Circuit n
| comp {n : Nat} (c1 : Circuit n) (c2 : Circuit n) : Circuit n
| tensorProduct {n m nm : Nat} (c1 : Circuit n) (c2 : Circuit m) (h : n + m = nm) : Circuit nm

[Kyle Miller]

The rule is "cases will work if all the indices appearing in constructors are made of free variables and constructor applications (after unfolding everything)". The issue is that + is not a constructor.