Well Founded Recursion New Problems

Stream: new members

[Joao Bregunci]

nce again, I am having a few problems with pattern matching. Here is a minimal working example:

inductive Role (AtomicRole : Type) : Type
  | Atomic  : AtomicRole → Role
  | Compose : Role → Role → Role
  | Inverse : Role → Role

inductive Concept (AtomicConcept AtomicRole : Type) : Type
  | Top           : Concept
  | Bot           : Concept
  | Atomic        : AtomicConcept → Concept
  | Negation      : Concept → Concept
  | Intersection  : Concept → Concept → Concept
  | Union         : Concept → Concept → Concept
  | Some          : (Role AtomicRole) → Concept → Concept
  | Every         : (Role AtomicRole) → Concept → Concept

inductive upper_Label (AC AR : Type) : Type
  | Empty : upper_Label
  | Negation : upper_Label
  | Forall : (Role AR) → Concept AC AR → upper_Label
  | Exist : (Role AR) → Concept AC AR → upper_Label

instance upper_Label_inhabited {AC AR : Type} :
  inhabited (upper_Label AC AR) := inhabited.mk upper_Label.Empty

structure lab_Concept (AC AR: Type) :=
mk :: (roles : list (upper_Label AC AR))
      (concept : Concept AC AR)

def sigma_line {AC AR : Type} : lab_Concept AC AR → upper_Label AC AR →  lab_Concept AC AR
  | a upper_Label.Empty           := a
  | a upper_Label.Negation        := lab_Concept.mk (a.roles.tail) (Concept.Negation a.concept)
  | a (upper_Label.Forall RO CO)  := lab_Concept.mk (a.roles.tail) (Concept.Every RO a.concept)
  | a (upper_Label.Exist RO CO)   := lab_Concept.mk (a.roles.tail) (Concept.Some RO a.concept)

def sigma_apply {AC AR : Type} (lc : @lab_Concept AC AR) :=
  sigma_line lc (lc.roles.head)

def sigma_line2 {AC AR : Type} : list (upper_Label AC AR) → lab_Concept AC AR → lab_Concept AC AR
  | [] a := a
  | ls a := sigma_line2 (ls.tail) (sigma_apply a)

def sigma_exhaust {AC AR : Type} (lb : lab_Concept AC AR) :=
  sigma_line2 lab_Concept.roles lab_Concept

I am having problems once again with pattern match in the function sigma_line2. I did read the page on using_well_founded, but I am still finding it extremely confusing on how to solve this issue, since the goal that I have found:

⊢ psigma.lex (λ (a₁ a₂ : list (upper_Label AC AR)), a₁.sizeof < a₂.sizeof)
    (λ (a : list (upper_Label AC AR)) (a₁ a₂ : lab_Concept AC AR),
       lab_Concept.sizeof AC AR a₁ < lab_Concept.sizeof AC AR a₂)
    ⟨ls.tail, sigma_apply a⟩
    ⟨ls, a⟩

Is not very intuitive. I tried inserting an attribute tag to a few definition before, but to no avail (this solved one previous issue of mine with notations). I think that the problem may be that it doesn't know that the tail of the list is going to be smaller, so that it is well defined the recursion of sigma_line2.

Just a few comments for the code. I have what I call a Concept and lab_Concept is a Concept together with a list of transformations on it. The first two sigma functions goal is to apply the first transformation in the lab_Concept and I only didn't make a single function, because I think that I can't do pattern match with lambdas in Lean 3 (math function in Lean 4). And the other two functions goal is to do all the applications until I get back a Concept.

So, any kind of ideas?

[Yakov Pechersky]

def sigma_line2 {AC AR : Type} : list (upper_Label AC AR) → lab_Concept AC AR → lab_Concept AC AR
  | [] a := a
  | (_ :: ls) a := sigma_line2 ls (sigma_apply a)

[Yakov Pechersky]

You can do the patterned deconstruction, which will help the equation compiler see that the term is decreasing, as opposed to deferring it into ls.tail and proving that operating on ls.tail decreases

[Joao Bregunci]

Awesome, really neat solution, really interesting how the equation compiler can solve this. But if I wanted to prove that these deferring and subsequent applications of tail would there be a more straightforward way? What I mean is making using of using_well_founded. Just asking for learning purposes, since I already stumbled in a similar problem in the past.

[Yakov Pechersky]

Something like

def sigma_line2 {AC AR : Type} : list (upper_Label AC AR) → lab_Concept AC AR → lab_Concept AC AR
  | [] a := a
  | ls a := let h := (show sizeof ls.tail < sizeof ls, by sorry) in
    sigma_line2 ls.tail (sigma_apply a)

or something about the using_well_founded { rel_tac := _ }

[Yakov Pechersky]

but in general, well-founded recursion definitions have worse computation, so it's not great if you have to rely on it

[Yakov Pechersky]

and sizeof ls.tail < sizeof ls isn't actually true, unless ls = (x :: xs) already