Proof inside a recursive function definition in order to ...

Stream: new members

[Saif Ghobash]

I am trying to define the notion of a context-free expression as an extension to regular-expressions to generate context-free languages. I am just toying around with it in LEAN but I am running into a few problems when trying to define the language generated by the expression (matches in the MWE). The issue here is that I need to show that a specific function is monotone but I need to make use of part of the definition of matches before it is actually fully defined. In the minimum working example code below, if you uncomment the first three lines in the proof you should be able to see what I mean:

import computability.language
import order.fixed_points


universes u v

variables {σ : Type u} {α : Type v}

-- Defined exactly like a regular_expression with the addition of
-- a var rule which takes a variable of type σ and a general recursion rule
-- which takes in a variable and a context_free_expression r to give μ x. r
-- The star operation is not needed since it can be expressed using the other rules.
inductive context_free_expression  (σ : Type u) (α : Type v)
| zero : context_free_expression
| epsilon : context_free_expression
| char : α → context_free_expression
| var  : σ → context_free_expression
| plus : context_free_expression → context_free_expression → context_free_expression
| comp : context_free_expression → context_free_expression → context_free_expression
| mu   : σ → context_free_expression → context_free_expression

namespace context_free_expression

instance : inhabited (context_free_expression σ α) := ⟨zero⟩

instance : has_add (context_free_expression σ α) := ⟨plus⟩
instance : has_mul (context_free_expression σ α) := ⟨comp⟩
instance : has_one (context_free_expression σ α) := ⟨epsilon⟩
instance : has_zero (context_free_expression σ α) := ⟨zero⟩

@[simp] lemma zero_def : (zero : (context_free_expression σ α)) = 0 := rfl
@[simp] lemma one_def : (epsilon : (context_free_expression σ α)) = 1 := rfl
@[simp] lemma plus_def (P Q : (context_free_expression σ α)) : plus P Q = P + Q := rfl
@[simp] lemma comp_def (P Q : (context_free_expression σ α)) : comp P Q = P * Q := rfl

-- This function takes in a context-free expression and an environment
-- η : σ → language α which maps variables to languages over α and returns
-- the corresponding context-free language.
def matches [decidable_eq σ] : context_free_expression σ α → (σ → language α) → language α
| 0 _ := 0
| 1 _ := 1
| (char a) _ := {[a]}
| (var x) η := η x
| (P + Q) η := P.matches η + Q.matches η
| (P * Q) η := P.matches η * Q.matches η
| (mu x r) η := order_hom.lfp
                    {
                      to_fun := (λ L : language α, matches r (λ y : σ, if y = x then L else η y)),
                      monotone' := by {
                        --intros a b hab x₁ hx₁,
                        --dsimp at *,
                        --induction r,
                        sorry,
                        -- The problem I have here is that I cannot "rw matches" even though
                        -- I have defined that matches zero _ := 0. There is a matches in the
                        -- list of hypotheses, but I do not know why it is there.
                      }
                    }

end context_free_expression

If anyone could shed some light on why this is the case, or give me a possible workaround that would be great.

[Patrick Johnson]

Try to change the return type of matches. Instead of returning language α, make it return a subtype that asserts that the corresponding function involving language α is monotone.