Proving property of function nested inside a function

Stream: general

[Mai]

I am not sure how to go about proving something like this (sorry for all the fluff definitions :smile:)

import Mathlib

structure TypeVar where
  n : Nat
deriving DecidableEq

mutual
  @[grind]
  structure PosUnion where
    types : List PosType

  inductive PosType where
    | func : List (TypeVar × List Constraint) -> NegType -> PosUnion -> PosType
    | var : TypeVar -> PosType

  inductive NegType where
    | var : TypeVar -> NegType

  inductive Constraint where
    | isFunc : PosType -> NegType -> Constraint
end

mutual
  def PosUnion.freeVars (u : PosUnion) : List TypeVar :=
    u.types.flatMap fun t => t.freeVars
  termination_by sizeOf u
  decreasing_by grind [List.sizeOf_lt_of_mem ‹t ∈ u.types›]

  def PosType.freeVars (τ : PosType) : List TypeVar :=
    match τ with
    | .func vars dom codom =>
      let bound := vars.unzip.1
      let consVars := vars.flatMap fun v => v.2.flatMap fun c => c.freeVars
      (consVars ∪ dom.freeVars ∪ codom.freeVars) \ bound
    | .var v => [v]
  termination_by sizeOf τ
  decreasing_by
    · grind [List.sizeOf_lt_of_mem ‹c ∈ v.snd›, List.sizeOf_lt_of_mem ‹v ∈ vars›]
    · decreasing_tactic

  def NegType.freeVars (τ : NegType) : List TypeVar :=
    match τ with
    | .var v => [v]
  termination_by sizeOf τ

  def Constraint.freeVars (c : Constraint) : List TypeVar :=
    match c with
    | .isFunc dom codom => dom.freeVars ∪ codom.freeVars
  termination_by sizeOf c
end

structure Ctx where
  types : List PosUnion

def Ctx.freeVars (Γ : Ctx) : List TypeVar :=
  Γ.types.flatMap PosUnion.freeVars

def reachableVars (Γ : Ctx) (cons : List (TypeVar × Constraint)) : List TypeVar :=
  let f s := s ∪ (cons
    |>.filter (fun c => c.1 ∈ s)
    |>.flatMap (fun c => c.2.freeVars))
  f^[cons.length] Γ.freeVars

lemma reachableVars_correct :
    let s := reachableVars Γ cons
    Γ.freeVars ⊆ s ∧ ∀ c ∈ cons, c.1 ∈ s -> c.2.freeVars ⊆ s := by
  apply And.intro
  · sorry
  · sorry

[Yury G. Kudryashov]

Could you please provide a summary of what's your issue? Is it the fact that f inside reachableVars isn't available as a separate entity to prove properties about it? If yes, then you can try using

def reachableVars ... :=
  f^[cons.length] Γ.freeVars
  where f := ...

syntax so that Lean defines reachableVars.f and you can prove lemmas about it before proving lemmas about reachableVars.

[Mai]

That's precisely the issue, I think. Thank you

[Mai]

I am still having a very hard time finishing this proof. any ideas what to do? nevermind, got it :laughing:

import Mathlib

structure TypeVar where
  n : Nat
deriving DecidableEq

mutual
  @[grind]
  structure PosUnion where
    types : List PosType

  inductive PosType where
    | func : List (TypeVar × List Constraint) -> NegType -> PosUnion -> PosType
    | var : TypeVar -> PosType

  inductive NegType where
    | var : TypeVar -> NegType

  inductive Constraint where
    | isFunc : PosType -> NegType -> Constraint
end

mutual
  def PosUnion.freeVars (u : PosUnion) : List TypeVar :=
    u.types.flatMap fun t => t.freeVars
  termination_by sizeOf u
  decreasing_by grind [List.sizeOf_lt_of_mem ‹t ∈ u.types›]

  def PosType.freeVars (τ : PosType) : List TypeVar :=
    match τ with
    | .func vars dom codom =>
      let bound := vars.unzip.1
      let consVars := vars.flatMap fun v => v.2.flatMap fun c => c.freeVars
      (consVars ∪ dom.freeVars ∪ codom.freeVars) \ bound
    | .var v => [v]
  termination_by sizeOf τ
  decreasing_by
    · grind [List.sizeOf_lt_of_mem ‹c ∈ v.snd›, List.sizeOf_lt_of_mem ‹v ∈ vars›]
    · decreasing_tactic

  def NegType.freeVars (τ : NegType) : List TypeVar :=
    match τ with
    | .var v => [v]
  termination_by sizeOf τ

  def Constraint.freeVars (c : Constraint) : List TypeVar :=
    match c with
    | .isFunc dom codom => dom.freeVars ∪ codom.freeVars
  termination_by sizeOf c
end

structure Ctx where
  types : List PosUnion

def Ctx.freeVars (Γ : Ctx) : List TypeVar :=
  Γ.types.flatMap PosUnion.freeVars

def reachableVars (Γ : Ctx) (cons : List (TypeVar × Constraint)) : List TypeVar :=
  f^[cons.length] Γ.freeVars
  where f s := s ∪ (cons.filter fun c => c.1 ∈ s).flatMap fun c => c.2.freeVars

lemma reachableVars_f_inflationary : s ⊆ reachableVars.f cons s := by
  intro v h
  exact List.mem_union_left h _

lemma reachableVars_includes_Γ_freeVars :
    Γ.freeVars ⊆ reachableVars Γ cons := by
  unfold reachableVars
  induction cons.length
  case zero => simp
  case succ prev =>
    sorry