Zulip Chat Archive

Stream: new members

Topic: Well Founded Recursion New Problems


view this post on Zulip Joao Bregunci (Mar 24 2021 at 17:01):

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?

view this post on Zulip Yakov Pechersky (Mar 24 2021 at 17:08):

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)

view this post on Zulip Yakov Pechersky (Mar 24 2021 at 17:09):

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

view this post on Zulip Joao Bregunci (Mar 24 2021 at 17:15):

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.

view this post on Zulip Yakov Pechersky (Mar 24 2021 at 17:41):

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 := _ }

view this post on Zulip Yakov Pechersky (Mar 24 2021 at 17:41):

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

view this post on Zulip Yakov Pechersky (Mar 24 2021 at 17:41):

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


Last updated: May 08 2021 at 09:11 UTC