Forall exists in assumption of an inductive

Stream: new members

[Harry Goldstein]

I'm trying to write a pretty complicated inductive definition for an evaluation relation of a programming language, and I think (unless I'm mistaken) that I can't really do it without some nested quantifiers in an argument:

import Batteries.Data.AssocList
open Batteries (AssocList)

inductive Value : Type :=
  | tt
  | ff
  | tuple (v₁ v₂ : Value)
  | nondet (vs : List Value)
deriving Repr, BEq, Inhabited

inductive Expr : Type :=
  | tt
  | ff
  | tuple (e₁ e₂ : Expr)
  | fst (e : Expr)
  | snd (e : Expr)
  | ifElse (e₁ e₂ e₃ : Expr)
  | ret (e : Expr)
  | var (x : String)
  | bind (x : String) (e₁ e₂ : Expr)
  | flip
deriving Repr, BEq, Inhabited

inductive Eval : AssocList String Value → Expr → Value → Prop
  | tt : Eval σ .tt .tt
  | ff : Eval σ .ff .ff
  | flip : Eval σ .flip (.nondet [.tt, .ff])
  | tuple :
    Eval σ e₁ v₁ →
    Eval σ e₂ v₂ →
    Eval σ (.tuple e₁ e₂) (.tuple v₁ v₂)
  | fst :
    Eval σ e (.tuple v₁ v₂) →
    Eval σ (.fst e) v₁
  | snd :
    Eval σ e (.tuple v₁ v₂) →
    Eval σ (.snd e) v₂
  | ifTrue :
    Eval σ e₁ .tt →
    Eval σ e₂ v →
    Eval σ (.ifElse e₁ e₂ e₃) v
  | ifFalse :
    Eval σ e₁ .ff →
    Eval σ e₃ v →
    Eval σ (.ifElse e₁ e₂ e₃) v
  | ret :
    Eval σ e v →
    Eval σ (.ret e) (.nondet [v])
  | var :
    σ.find? x = some v →
    Eval σ (.var x) v
  | bind :
    Eval σ e₁ (.nondet vs₁) →
    (∀ v ∈ vs, ∃ v₁ ∈ vs₁, Eval (σ.cons x v₁) e₂ (.nondet vs₂) ∧ v ∈ vs₂) →
    Eval σ (.bind x e₁ e₂) (.nondet vs)

Lean complains about "invalid nested inductive datatype 'Exists', nested inductive datatypes parameters cannot contain local variables", and I think I see the logic for why, but I'm not sure if and how I can express something equivalent that Lean can handle.

[Shanghe Chen]

It seems the problem happened in the bind constructor. If it's commented then no error is reported

[Harry Goldstein]

Yes, but I do need the bind constructor...

[Shanghe Chen]

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.E2.9C.94.20Type.20Mismatch.3F a quite old thread seems containing a similar error.

[Harry Goldstein]

Yes, I think these issues do seem related. Although in this case I'm not sure I understand how to unravel the inductive in the same way. If there are other examples of this kind of thing in practice that would be super helpful

[Shanghe Chen]

Hi have you solved the problem? Or could you please share the background of the problem, or simplify the programming language but still with the problematic issue?

[Harry Goldstein]

No, unfortunately I haven't yet. The core problem, I think, is that I need to encode the ∀∃ in the bind constructor as a separate mutually-inductive relation, but I'm not really sure how to do that. I encoded the relation as a function for now (it's really just bind in the List monad a couple of times) but someday I would like to figure out the right way to write this as an inductive.

[Shanghe Chen]

I am wondering if it’s #xy or not. Could you please share the original programming language, it’s kind of like untyped lambda calculus? And what’s the main result wanna to prove?

[Harry Goldstein]

It's a nondeterministic calculus, and I'm trying to prove that its semantics is equivalent to the semantics of the same program compiled to a lower-level language. But really the main important thing is that the bind constructor evaluates its first argument, then for any v₁ that argument could evaluate to it evaluates its second argument with v₁ appended to the context, and finally it joins all of those lists together. This is what the interpretation looks like as a function:

def Expr.interp (e : Expr) (σ : AssocList String Value) : Option Value :=
  match e with
  ...
  | .bind x e₁ e₂ => do
    let .nondet vs ← e₁.interp σ | none
    let vss ← vs.mapM (λ v => do
      let .nondet vs' ← e₂.interp (σ.cons x v) | none
      pure vs')
    pure (.nondet vss.join)

The inductive I posted tries to capture the same thing, just by constraining the values in the output list, since I don't think it makes sense to map a relation over a list.

Does that help? I don't think I'm too far off base with what I'm trying to do, I just don't know the right way to do it.

[Shanghe Chen]

I dont know if I understand the original problem correctly or not. Does using more inductive construction and avoiding Exist and Forall in the definition of Eval help? Maybe the definition of it should be totally inductively built up. I did an exercise for the nondeterministic addtion of two list too. It's kind of tautological to me:

abbrev Var := String
abbrev Values := List Nat

/--
all expressions have forms like:
- value, like [1,2,3]
- variable, like "x"
- operations, here simply an addition
- a bind epression, which means that
  the expression e1 will be evaluated,
  and bind to the variable x
-/
inductive Expr : Type
| val (vs : Values)
| var (x : Var)
| add (e1 e2: Expr)
| bind (x: Var) (e1 e2 : Expr)

/--
The context gives each variable a result containing nondeterministic values
-/
abbrev Context := Var -> Values

/-- the auxiliary definition for nondeterministic addition  -/
def add : Values -> Values -> Values
| [], _ => []
| (x::xs), ys => List.map (x + ·) ys ++ add xs ys

/--
update the context for variable x
-/
def bind (c: Context) (x: Var) (vs : Values) : Context :=
fun y => if y = x then vs else c y

/--
inductively define the evaluation proposition, a term of
`derive ctx expr vs` means that under the context `ctx`, the `expr`
should be evaluated to `vs`
Here the inductive families should represent the sematic for the real
evaluation, i.e, a prop in the families has term(or, terms, for Prop has only one term)
iff it does evaluated to the values
-/
inductive derive : Context -> Expr -> Value -> Prop
| val c vs: derive c (.val vs) vs
| var c x: derive c (.var x) (c x)
| add c e1 e2 vs1 vs2:
   derive c e1 vs1 -> derive c e2 vs2
   -> derive c (.add e1 e2) (add vs1 vs2)
/-- for `.bind x e1 e2`, only `e1` evaluated to some `vs1` and after
 binding it to `x`, `e2` evalued to some `vs2`
 -/
| bind c e1 e2 vs1 vs2 x:
   derive c e1 vs1 -> derive (bind c x vs1) e2 vs2
   -> derive c (.bind x e1 e2) vs2

def c0 : Context
| _ => []

abbrev x:= "x"
abbrev y:= "y"

example : derive c0 (.bind x (.val [1,2,3]) (.bind y (.val [4,5,6]) (.add (.var x) (.var y)))) [5,6,7,6,7,8,7,8,9] := by
  apply derive.bind
  apply derive.val
  apply derive.bind
  apply derive.val
  have eq: add [1,2,3] [4,5,6] = [5,6,7,6,7,8,7,8,9] := by rfl
  rw [←eq]
  apply derive.add
  apply derive.var
  apply derive.var

/--
real evaluatation
-/
def eval (c: Context) : Expr -> Values
| .val vs => vs
| .var x => c x
| .add x y => add (eval c x) (eval c y)
| .bind x e1 e2 => eval (bind c x (eval c e1)) e2

def comp (c: Context) (vs: Values) : (e: Expr) -> derive c e vs ↔ eval c e = vs
| .val vs => by
  constructor
  . intro ev
    cases ev
    simp [eval]
  . intro ev
    rw [←ev]
    apply derive.val
| .var x => by
  constructor
  . intro ev
    cases ev
    simp [eval]
  . intro ev
    rw [←ev]
    apply derive.var
| .add x y => by
  constructor
  . intro ev
    cases ev
    simp [eval]
    rw [(comp c _ x).mp (by assumption)]
    rw [(comp c _ y).mp (by assumption)]
  . intro ev
    cases ev
    apply derive.add
    apply (comp ..).mpr
    rfl
    apply (comp ..).mpr
    rfl
| .bind x e1 e2 => by
  constructor
  . intro ev
    cases ev
    simp [eval]
    rw [(comp c _ e1).mp (by assumption)]
    rw [(comp _ _ e2).mp (by assumption)]
  . intro ev
    cases ev
    apply derive.bind
    apply (comp c (eval c e1) _).mpr
    rfl
    apply (comp ..).mpr
    rfl

[Harry Goldstein]

The problem is that the semantics of the language isn't 100% nondeterministic. There are deterministic values like true and nondeterministic ones specified by nondet. I'm mimicking the behavior you'd get with the Gen monad in a library like QuickCheck (I'm not sure if Lean has an equivalent). Anyway, I really don't think it's worth your time to try to understand why the semantics I wrote is the one I want---I just want to know if Lean can represent it.