cannot mix theorems and definitions

Stream: new members

[Yiftach S]

Hello! I noticed I cannot use mutual on a function with a theorem.
I want to write a recursive function, that uses a theorem about itself.
Is there any way to do that?

[Junyan Xu]

Can you provide a #mwe? Without knowing your exact problem, I guess it might help to define a function to a docs#Subtype.

[Yiftach S]

Junyan Xu said:

Can you provide a #mwe? Without knowing your exact problem, I guess it might help to define a function to a docs#Subtype.

Sure thing. My full code is much longer, but this a simplification of the issue:

inductive MyBinTree where
  | leaf
  | node (left : MyBinTree) (key : Nat) (right : MyBinTree)


def MyBinTree.sizeOf : MyBinTree → Nat
  | .leaf => 0
  | .node l _ r => 1 + l.sizeOf + r.sizeOf

def func (t : MyBinTree) : MyBinTree :=
  match ht : t with
  | .leaf => .leaf
  | .node left key right =>
    let t1 := func left
    -- Here I'd like to use func_size, but func and func_size cannot be mutual
    have help : left.sizeOf = t1.sizeOf := sorry
    t

theorem func_size (t : MyBinTree) : t.sizeOf = (func t).sizeOf :=
  sorry

[Junyan Xu]

In your example the constructors of MyBinTree doesn't require any proofs, so it's not clear why you'd like to use a theorem to define func. Can you not define func first and prove func_size later? If not then I'm afraid I can't provide suggestions without a more detailed example that include the essential difficulty.

[Yiftach S]

Junyan Xu said:

In your example the constructors of MyBinTree doesn't require any proofs, so it's not clear why you'd like to use a theorem to define func. Can you not define func first and prove func_size later? If not then I'm afraid I can't provide suggestions without a more detailed example that include the essential difficulty.

Thanks. The issue is that func is recursive, and it needs a proof about what it does in order to work.
I'll also add my actual problem, but it's rather long so I thought that the shorter version might be easier to respond to.
The problems are marked with "TODO".

import Mathlib.Tactic.Linarith
import Mathlib.Algebra.Order.Monoid.Lemmas


inductive TreeBin where
  | leaf
  | node (left : TreeBin) (key : Nat) (right : TreeBin)


def TreeBin.repr : TreeBin → String
| TreeBin.leaf => "" --"."
| TreeBin.node l k r => "(" ++ TreeBin.repr l ++ (Nat.repr k) ++ TreeBin.repr r ++ ")"



def TreeBin.sizeOf : TreeBin → Nat
  | .leaf => 0
  | .node l _ r => 1 + l.sizeOf + r.sizeOf


-- t1 ≤ t2 definition by key
instance : LE TreeBin where
  le t1 t2 :=
  match t1, t2 with
  | .leaf, _ => true
  | .node _ _ _, .leaf => false
  | .node _ k1 _, .node _ k2 _ => k1 ≤ k2


-- Unfolding TreeBin comparison
macro "unfold_ge" : tactic => `(tactic| (unfold GE.ge LE.le instLETreeBin))
macro "unfold_le" : tactic => `(tactic| (unfold LE.le instLETreeBin))


theorem not_ge {a b : TreeBin} : (¬(a ≥ b)) → (b ≥ a) := by
  intro h
  match ha : a, hb : b with
  | .leaf, _ => unfold_ge; trivial
  | .node _ _ _, .leaf => let h3 : ¬ (a ≥ b) := by simp [ha, hb, h]
                          let h2 : a ≥ b := by unfold_ge; trivial
                          exact absurd h2 h3
  | .node _ k1 _, .node _ k2 _ => unfold_ge; simp [ha, hb];
                                  sorry



-- LE is decidable
instance TreeBin.decLE (t₁ t₂ : TreeBin) : Decidable (t₁ ≤ t₂) :=
  match t₁, t₂ with
  | .leaf, _ => by simp [LE.le]; exact isTrue True.intro
  | .node _ _ _, .leaf =>  by simp [LE.le]; exact isFalse False.elim
  | .node _ k1 _, .node _ k2 _ => Nat.decLe k1 k2


-- Local max heap definition - the node doesn't have direct children that are bigger
def local_max (t : TreeBin) : Prop :=
  match t with
  | .leaf => True
  | .node l _ r => (t ≥ l) ∧ (t ≥ r)


-- local_max is decidable
instance decidable_local_max (t : TreeBin) : Decidable (local_max t) :=
  match t with
  | .leaf => by simp [local_max]; exact isTrue True.intro
  | .node l _ r => instDecidableAnd


-- max heap condition - local_max and children are also max heaps
inductive is_max_heap : TreeBin → Prop
 | leaf : is_max_heap .leaf
 | node : local_max (.node left key right) →
          is_max_heap left → is_max_heap right →
          is_max_heap (.node left key right)


def MaxHeap := { t : TreeBin // is_max_heap t }


-- Proof that LE is transitive for TreeBin
theorem trans_le {a b c : TreeBin} : a ≤ b → b ≤ c → a ≤ c := by
  intro h1 h2
  cases a with
  | leaf => trivial -- A leaf is always little
  | node al ak ar =>
    cases b with
    | leaf => trivial -- b being a leaf contradicts a ≤ b
    | node bl bk br =>
      cases c with
      | leaf => trivial -- c being a leaf contradicts b ≤ c
      -- All 3 are nodes, so this is the final case which is simply comparing numbers
      | node cl ck cr => exact Nat.le_trans h1 h2

-- Make lean use trans_le
instance : Trans (LE.le : TreeBin → TreeBin → Prop) (LE.le : TreeBin → TreeBin → Prop) (LE.le : TreeBin → TreeBin → Prop) where
  trans := fun p q => trans_le p q

-- Same but for GE
instance : Trans (GE.ge : TreeBin → TreeBin → Prop) (GE.ge : TreeBin → TreeBin → Prop) (GE.ge : TreeBin → TreeBin → Prop) where
  trans := fun p q => trans_le q p


theorem plus_le1 (a b : Nat) : a < 1 + a + b := by
  linarith

theorem plus_le2 (a b : Nat) : b < 1 + a + b := by
  linarith


-- Convert a TreeBin to a heap recursively
def heapify (t : TreeBin) : MaxHeap :=
  match ht : t with
  | .leaf => ⟨.leaf, by simp [is_max_heap.leaf]⟩
  | .node left key right =>
    -- used to prove termination
    have left_l_t : left.sizeOf < t.sizeOf := by
      conv in TreeBin.sizeOf t => unfold TreeBin.sizeOf
      simp [ht, plus_le1]
    have _ : right.sizeOf < t.sizeOf := by
      conv in TreeBin.sizeOf t => unfold TreeBin.sizeOf
      simp [ht, plus_le2]
    -- recursively heapify children
    let l1 := heapify left
    let r1 := heapify right
    -- a default return value in case local_max is OK
    let ret_t_default := TreeBin.node l1.val key r1.val
    if default_local_max : local_max ret_t_default then
      ⟨ret_t_default, by
      simp [is_max_heap.node, default_local_max, l1.property, r1.property]⟩
    -- Second case l2 on top
    else if l1_ge_r1 : l1.val ≥ r1.val then
      match hl1 : l1.val with
      | .leaf => by  -- l1 being a leaf is absurd
        have ret_ge_l1 : ret_t_default ≥ l1.val := by unfold_ge; simp [hl1]
        have ret_ge_r1 : ret_t_default ≥ r1.val := by calc _ ≥ l1.val := ret_ge_l1
                                                           _ ≥ r1.val := l1_ge_r1
        have ret_local_max : local_max ret_t_default := by simp [local_max, ret_ge_l1, ret_ge_r1]
        exact absurd ret_local_max default_local_max
      | .node ll lk lr =>
        let l2_t := TreeBin.node ll key lr
        have _ : l2_t.sizeOf < t.sizeOf := calc _ = l1.val.sizeOf := by unfold TreeBin.sizeOf; simp [hl1]
                                                -- TODO: how to prove that heapify doesn't change the size?
                                                _ = left.sizeOf := by sorry
                                                _ < t.sizeOf := left_l_t
        let l2 := heapify l2_t
        let ret_t := TreeBin.node l2.val lk r1.val

        -- TODO: I didn't manage to complete this proof.
        --       l2_t consists of ll + lr + key.
        --       key is smaller than lk because of default_local_max + l1_ge_r1.
        --       ll and lr are recursively smaller than lk because l1 is a max heap.
        --       This proves that l1 is greater than ANY value in l2_t, and heapify doesn't add any values.
        have l1_ge_l2 : l1.val ≥ l2.val := by sorry

        let local_max_ret_t : local_max ret_t := by {
          unfold local_max;
          apply And.intro
          · calc ret_t ≥ l1.val := by unfold_ge; simp [hl1]
                 _ ≥ l2.val := l1_ge_l2
          · calc ret_t ≥ l1.val := by unfold_ge; simp [hl1]  -- Same key
                 _ ≥ r1.val := l1_ge_r1
        }
        ⟨ret_t, by simp [is_max_heap.node, l2.property, r1.property, local_max_ret_t]⟩
    -- Final case r1 on top
    -- I didn't bother with this as much, because the privious case is similar
    else
      match hr1 : r1.val with
      | .leaf => by  -- l1 being a leaf is absurd
        have ret_ge_r1 : ret_t_default ≥ r1.val := by unfold_ge; simp [hr1]
        have ret_ge_l1 : ret_t_default ≥ l1.val := by calc _ ≥ r1.val := ret_ge_r1
                                                           _ ≥ l1.val := not_ge l1_ge_r1
        have ret_local_max : local_max ret_t_default := by simp [local_max, ret_ge_l1, ret_ge_r1]
        exact absurd ret_local_max default_local_max
      | .node rl rk rr =>
        let r2_t := TreeBin.node rl key rr
        have _ : r2_t.sizeOf < t.sizeOf := sorry
        let r2 := heapify r2_t
        let ret_t := TreeBin.node l1.val rk r2.val
        let local_max_ret_t : local_max ret_t := by sorry
        ⟨ret_t, by simp [is_max_heap.node, r2.property, l1.property, local_max_ret_t]⟩
  termination_by t.sizeOf

[Kyle Miller]

I think Junyan's subtype suggestion would be to define def heapifyAux (t : TreeBin) : {mh : MaxHeap // mh.val.sizeOf = t.sizeOf} to interleave the proof with the definition.

[Yiftach S]

Kyle Miller said:

I think Junyan's subtype suggestion would be to define def heapifyAux (t : TreeBin) : {mh : MaxHeap // mh.val.sizeOf = t.sizeOf} to interleave the proof with the definition.

Oh, I didn't realize you could define a subtype while returning it. This indeed solves the problem, Thanks!

I still doubt I'll manage the second TODO (the long one).
I need to show that heapify doesn't change the values and adds something bigger than there used to be in the tree. Is there any elegant way to go about that?

[Junyan Xu]

(deleted)

[Junyan Xu]

Hopefully this helps:

/-- Define the set of values inductively. -/
def TreeBin.values : TreeBin → Set Nat
  | .leaf => ∅
  | .node left key right => left.values ∪ {key} ∪ right.values

/-- Define `heapify` without incorporating the is_max_heap condition; it's easier to prove it separately. -/
def heapify (t : TreeBin) : {t' : TreeBin // t'.sizeOf = t.sizeOf} :=
  match ht : t with
  | .leaf => ⟨.leaf, by simp⟩
  | .node left key right =>
    have : left.sizeOf < t.sizeOf := by
      conv in TreeBin.sizeOf t => unfold TreeBin.sizeOf
      simp [ht, plus_le1]
    have : right.sizeOf < t.sizeOf := by
      conv in TreeBin.sizeOf t => unfold TreeBin.sizeOf
      simp [ht, plus_le2]
    let l1 := heapify left
    let r1 := heapify right
    let ret_t_default : {t' : TreeBin // t'.sizeOf = (TreeBin.node left key right).sizeOf} :=
      ⟨TreeBin.node l1 key r1, by simp_rw [TreeBin.sizeOf, l1.2, r1.2]⟩
    if local_max ret_t_default then ret_t_default
    else if l1.val ≥ r1.val then
      match hl1 : l1.val with
      | .leaf => ret_t_default -- this can't happen, you're free to put any value
      | .node ll lk lr =>
        let l2_t := TreeBin.node ll key lr
        have : l2_t.sizeOf < t.sizeOf := by
          have hl1 := congr_arg TreeBin.sizeOf hl1
          rw [TreeBin.sizeOf] at hl1
          simp_rw [ht, TreeBin.sizeOf, ← hl1, l1.2, plus_le1]
        ⟨TreeBin.node (heapify l2_t).val lk r1, by
          simp [TreeBin.sizeOf, (heapify l2_t).2, r1.2, ← l1.2, hl1]⟩
    else match hr1 : r1.val with
      | .leaf => ret_t_default -- can't happen
      | .node rl rk rr =>
        let r2_t := TreeBin.node rl key rr
        have : r2_t.sizeOf < t.sizeOf := by
          have hr1 := congr_arg TreeBin.sizeOf hr1
          rw [TreeBin.sizeOf] at hr1
          simp_rw [ht, TreeBin.sizeOf, ← hr1, r1.2, plus_le2]
        ⟨TreeBin.node l1 rk (heapify r2_t), by
          simp [TreeBin.sizeOf, (heapify r2_t).2, l1.2, ← r1.2, hr1]⟩
termination_by t.sizeOf

/-- We can now state the fact that `heapify` preserves the set of values. -/
lemma values_heapify (t : TreeBin) : (heapify t).1.values = t.values := sorry

[Yiftach S]

Junyan Xu said:

Hopefully this helps:

/-- Define the set of values inductively. -/
def TreeBin.values : TreeBin → Set Nat
  | .leaf => ∅
  | .node left key right => left.values ∪ {key} ∪ right.values

/-- Define `heapify` without incorporating the is_max_heap condition; it's easier to prove it separately. -/
def heapify (t : TreeBin) : {t' : TreeBin // t'.sizeOf = t.sizeOf} :=
  match ht : t with
  | .leaf => ⟨.leaf, by simp⟩
  | .node left key right =>
    have : left.sizeOf < t.sizeOf := by
      conv in TreeBin.sizeOf t => unfold TreeBin.sizeOf
      simp [ht, plus_le1]
    have : right.sizeOf < t.sizeOf := by
      conv in TreeBin.sizeOf t => unfold TreeBin.sizeOf
      simp [ht, plus_le2]
    let l1 := heapify left
    let r1 := heapify right
    let ret_t_default : {t' : TreeBin // t'.sizeOf = (TreeBin.node left key right).sizeOf} :=
      ⟨TreeBin.node l1 key r1, by simp_rw [TreeBin.sizeOf, l1.2, r1.2]⟩
    if local_max ret_t_default then ret_t_default
    else if l1.val ≥ r1.val then
      match hl1 : l1.val with
      | .leaf => ret_t_default -- this can't happen, you're free to put any value
      | .node ll lk lr =>
        let l2_t := TreeBin.node ll key lr
        have : l2_t.sizeOf < t.sizeOf := by
          have hl1 := congr_arg TreeBin.sizeOf hl1
          rw [TreeBin.sizeOf] at hl1
          simp_rw [ht, TreeBin.sizeOf, ← hl1, l1.2, plus_le1]
        ⟨TreeBin.node (heapify l2_t).val lk r1, by
          simp [TreeBin.sizeOf, (heapify l2_t).2, r1.2, ← l1.2, hl1]⟩
    else match hr1 : r1.val with
      | .leaf => ret_t_default -- can't happen
      | .node rl rk rr =>
        let r2_t := TreeBin.node rl key rr
        have : r2_t.sizeOf < t.sizeOf := by
          have hr1 := congr_arg TreeBin.sizeOf hr1
          rw [TreeBin.sizeOf] at hr1
          simp_rw [ht, TreeBin.sizeOf, ← hr1, r1.2, plus_le2]
        ⟨TreeBin.node l1 rk (heapify r2_t), by
          simp [TreeBin.sizeOf, (heapify r2_t).2, l1.2, ← r1.2, hr1]⟩
termination_by t.sizeOf

/-- We can now state the fact that `heapify` preserves the set of values. -/
lemma values_heapify (t : TreeBin) : (heapify t).1.values = t.values := sorry

Thanks! That's seems to be the way to do it