Unexpected pattern matching behaviour

Stream: new members

[Julian Sutherland]

I'm working with a complex type family:

....
inductive TType : Type
| BlockList : FTContext → finset Identifier → finset Identifier → TType
| CBlock : FTContext → finset Identifier → TType
| SwitchBody : FTContext → finset Identifier → TType
| CExpr : FTContext → finset Identifier → ℕ → TType
| CStatement : FTContext → finset Identifier → finset Identifier → TType

open TType

inductive Yulℂ : TType → Type
| EmpCBlock : ∀ (Γ : FTContext) (vars : finset Identifier), Yulℂ (BlockList Γ vars vars)
| SeqCBlock  :
  ∀ (Γ : FTContext) (vars : finset Identifier) (vars' : finset Identifier) (vars'' : finset Identifier),
    Yulℂ (CStatement Γ vars vars') -> Yulℂ (BlockList Γ vars' vars'') → Yulℂ (BlockList Γ vars vars'')

| NestedScope : ∀ (Γ : FTContext) (vars inner_vars inner_vars' : finset Identifier),
    VarStore inner_vars → Yulℂ (BlockList Γ (inner_vars ∪ vars) (inner_vars' ∪ vars)) → Yulℂ (CBlock Γ vars)

| CCase : ∀ (Γ : FTContext) (vars : finset Identifier),
    Literal → Yulℂ (CBlock Γ vars) → Yulℂ (SwitchBody Γ vars) → Yulℂ (SwitchBody Γ vars)
| CDefault : ∀ (Γ : FTContext) (vars : finset Identifier),
    Yulℂ (CBlock Γ vars) → Yulℂ (SwitchBody Γ vars)

| CFunctionCall : ∀ (Γ : FTContext) (vars : finset Identifier)
                    (f_id : Identifier) (n : ℕ) (m : ℕ),
    (Γ f_id = some (n,m)) →
    (fin n → Yulℂ (CExpr Γ vars 1)) →
    Yulℂ (CExpr Γ vars m)
| CId : ∀ (Γ : FTContext) (vars : finset Identifier) (id : Identifier), id ∈ vars → Yulℂ (CExpr Γ vars 1)
| CLit : ∀ (Γ : FTContext) (vars : finset Identifier), Literal → Yulℂ (CExpr Γ vars 1)
| Scope : ∀ (Γ : FTContext) (vars_outer vars_inner vars_inner' : finset Identifier)
               (m : ℕ) (ret_vars : fin m → Identifier),
    VarStore (vars_inner ∪ (tofinset ret_vars)) →
    Yulℂ (CStatement Γ (vars_inner ∪ (tofinset ret_vars)) (vars_inner' ∪ (tofinset ret_vars))) →
    Yulℂ (CExpr Γ vars_outer m)

| CBlock : ∀ (Γ : FTContext) (vars : finset Identifier), Yulℂ (CBlock Γ vars) → Yulℂ (CStatement Γ vars vars)
  -- Function definitions already parsed into FTContext.
| CVariableDeclarationAss :
    ∀ (Γ : FTContext) (vars : finset Identifier) (n : ℕ) (new_vars : fin n -> Identifier),
      Yulℂ (CExpr Γ vars n) →  Yulℂ (CStatement Γ vars (vars ∪ (tofinset new_vars)))
| CVariableDeclaration :
    ∀ (Γ : FTContext) (vars : finset Identifier) (n : ℕ) (new_vars : fin n -> Identifier),
      Yulℂ (CStatement Γ vars (vars ∪ (tofinset new_vars)))
| CAssignment : ∀ (Γ : FTContext) (vars : finset Identifier) (n : ℕ) (ids : fin n -> Identifier),
    tofinset ids ⊆ vars → Yulℂ (CExpr Γ vars n) → Yulℂ (CStatement Γ vars vars)
| CIf : ∀ (Γ : FTContext) (vars : finset Identifier),
    Yulℂ (CExpr Γ vars 1) → Yulℂ (CBlock Γ vars) → Yulℂ (CStatement Γ vars vars)
| CExpressionStatement : ∀ (Γ : FTContext) (vars : finset Identifier),
    Yulℂ (CExpr Γ vars 0) -> Yulℂ (CStatement Γ vars vars)
| CSwitch : ∀ (Γ : FTContext) (vars : finset Identifier),
    Yulℂ (CExpr Γ vars 1) →
    Yulℂ (SwitchBody Γ vars) →
    Yulℂ (CStatement Γ vars vars)
| CFor : ∀ (Γ : FTContext) (vars vars' vars'' vars''' : finset Identifier),
    Yulℂ (BlockList Γ vars vars') → Yulℂ (CExpr Γ vars' 1) →
    Yulℂ (BlockList Γ vars' vars'') → Yulℂ (BlockList Γ vars'' vars''') →
    Yulℂ (CStatement Γ vars vars)
| CBreak : ∀ (Γ : FTContext) (vars : finset Identifier), Yulℂ (CStatement Γ vars vars)
| CContinue : ∀ (Γ : FTContext) (vars : finset Identifier), Yulℂ (CStatement Γ vars vars)
| CLeave : ∀ (Γ : FTContext) (vars : finset Identifier), Yulℂ (CStatement Γ vars vars)
| ForCheckCond : ∀ (Γ : FTContext) (vars : finset Identifier),
    Yulℂ (CExpr Γ vars 1) → Yulℂ (BlockList Γ vars vars) -> Yulℂ (CExpr Γ vars 1) ->
    Yulℂ (CStatement Γ vars vars)
| ForExecBody : ∀ (Γ : FTContext) (vars : finset Identifier),
    Yulℂ (CExpr Γ vars 1) → Yulℂ (BlockList Γ vars vars) →
    Yulℂ (CStatement Γ vars vars) -> Yulℂ (CStatement Γ vars vars)
| Skip : ∀ (Γ : FTContext) (vars : finset Identifier), Yulℂ (CStatement Γ vars vars)

I'm getting some rather confusing pattern matching behaviour that I do not know how to get around.
When I define the function is_evaluated:

def is_evaluated : ∀ {t : TType}, Yulℂ t → Prop
| (BlockList _ _ _) (EmpCBlock _ _) := true
| (BlockList _ _ _) _               := false
| (CBlock _ _) (NestedScope _ _ _ _ _ blklst) := is_evaluated blklst
| (SwitchBody _ _) _ := false
| (CExpr _ _ _) (CLit _ _ _) := true
| (CExpr _ _ _) (CId _ _ _ _) := false
| (CExpr _ _ n) (Scope _ _ _ _ _ _ _ cstmnt) := (n ≠ 1) ∧ is_skip cstmnt
| (CExpr _ _ _) _ := false
| (CStatement _ _ _) cstmnt := is_skip cstmnt
| (CStatement _ {val := _, nodup := _} {val := _, nodup := _}) _ := false

Lean gives me the error

non-exhaustive match, the following cases are missing:
is_evaluated (CStatement _ {val := _, nodup := _} {val := _, nodup := _}) _

Note that this pattern match is _exactly_ the last pattern match of this function. I'm not sure how to approach fixing this any advice is much appreciated :)

[Huỳnh Trần Khanh]

argh... I already told you in another thread, programming language semantics is incredibly messy to deal with :joy: hey but I have a trick!

[Huỳnh Trần Khanh]

enter tactic mode

[Huỳnh Trần Khanh]

instead of defining is_evaluated using pattern matching, try using := begin ... end instead

[Huỳnh Trần Khanh]

then, inside the begin ... end block, type intros then cases on a variable

[Huỳnh Trần Khanh]

that variable will split into multiple variants and you can deal with each of them individually

[Huỳnh Trần Khanh]

the equation compiler is sometimes weird lol

[Huỳnh Trần Khanh]

basically the rule of thumb is if the equation compiler does something weird, enter tactic mode, if tactic mode does something weird, use the equation compiler :joy:

[Huỳnh Trần Khanh]

if you have nowhere to go, use recursors directly I guess but I've never had to do that

[Chris B]

What does the error look like if you set set_option pp.all true?

[Julian Sutherland]

Thanks! I gave that a try and got:

non-exhaustive match, the following cases are missing:
is_evaluated (TType.CStatement _ (@finset.mk.{0} Identifier _ _) (@finset.mk.{0} Identifier _ _)) _

So I then tried:

def is_evaluated : ∀ {t : TType}, Yulℂ t → Prop
| (BlockList _ _ _) (EmpCBlock _ _) := true
| (BlockList _ _ _) _               := false
| (CBlock _ _) (NestedScope _ _ _ _ _ blklst) := is_evaluated blklst
| (SwitchBody _ _) _ := false
| (CExpr _ _ _) (CLit _ _ _) := true
| (CExpr _ _ _) (CId _ _ _ _) := false
| (CExpr _ _ n) (Scope _ _ _ _ _ _ _ cstmnt) := (n ≠ 1) ∧ is_skip cstmnt
| (CExpr _ _ _) _ := false
| (CStatement _ _ _) cstmnt := is_skip cstmnt
| is_evaluated (CStatement _ (finset.mk.{0} _ _) (finset.mk.{0} _ _)) _ :=
  false

But I then get ill-formed match/equation expression on the first line of the pattern match... However, I can't see why that is... (Note that I have insert open TType right after the definition of TType)

[Chris B]

The last case shouldn't have is_evaluated on the left.

[Julian Sutherland]

Apologies! Sorry I copy and pasted the match suggested by the error message without paying enough attention!
Now

def is_evaluated : ∀ {t : TType}, Yulℂ t → Prop
| (BlockList _ _ _) (EmpCBlock _ _) := true
| (BlockList _ _ _) _               := false
| (CBlock _ _) (NestedScope _ _ _ _ _ blklst) := is_evaluated blklst
| (SwitchBody _ _) _ := false
| (CExpr _ _ _) (CLit _ _ _) := true
| (CExpr _ _ _) (CId _ _ _ _) := false
| (CExpr _ _ n) (Scope _ _ _ _ _ _ _ cstmnt) := (n ≠ 1) ∧ is_skip cstmnt
| (CExpr _ _ _) _ := false
| (CStatement _ _ _) cstmnt := is_skip cstmnt
| (CStatement _ (finset.mk.{0} _ _) (finset.mk.{0} _ _)) _ := false

Gives me

non-exhaustive match, the following cases are missing:
is_evaluated (TType.CStatement _ (@finset.mk.{0} Identifier _ _) (@finset.mk.{0} Identifier _ _)) _

while also reporting

equation compiler error, equation #10 has not been used in the compilation (possible solution: delete equation)

on the last line of the match, so same situation as before.

[Julian Sutherland]

@Huỳnh Trần Khanh I gave that a try, while it works, the generated equations are extremely large and quite difficult to use practically in proofs it seems... Thanks :)

[Chris B]

It's hard to troubleshoot without the whole thing being available; assuming Identifier is actually being inferred in the one you're writing (you can try @finset.mk.{0} Identifier _ _), one other thing you can do it make the last arm a wildcard _ to get it to typecheck and try to observe the definition to see how it's different from what you were trying to write.

[Julian Sutherland]

Apologies, Identifier is simply a string :)

I tried

| (CStatement _ (@finset.mk.{0} Identifier _ _) (finset.mk.{0} _ _)) _ := false

which resulted in the same situation. However, I was surprised that when I initially did:

| (CStatement _ (@finset.mk.{0} Identifier _ _) (@finset.mk.{0} Identifier _ _)) _ := false

I got the same errors as before, but also:

invalid pattern, 'Identifier' already appeared in this pattern

Which indicates that Lean seems to be interpreting this as a binding rather than a pattern?

[Chris B]

Is Identifier in a namespace?

[Julian Sutherland]

It is yes, it's used a number of times in this file, including in the definition of the Yulℂ type family :)

[Chris B]

If the namespace isn't open in the segment in which you write is_evaluated (unsure based on the example) you'll have to address Identifier by its full name.

[Julian Sutherland]

This same issue occurs if I use the (equivalent) pattern:

| (CStatement _ (@finset.mk.{0} string _ _) (@finset.mk.{0} string _ _)) _ := false

and I imagine that string is in scope by default from core.

[Julian Sutherland]

and, in fact, also occurs if I move the definition of Identifier into this file (so that it is definitely in the current namespace).

[Chris B]

I took the pretty-printer's bait. You've stumped me; you might want to post the full code somewhere since it seems difficult to resolve by eyeballing it.

[Julian Sutherland]

So, the only other relevant code is the preamble of the file and the definition of is_skip:

import tactic.linarith

import data.finset.basic
import data.vector
import init.data.fin.ops
import init.data.list.basic

def UInt256_max : ℕ := 2^256
def UInt256 := fin UInt256_max
def Literal := UInt256
def Identifier := string

lemma zero_lt_uint256_max : 0 < UInt256_max :=
  begin
    cases (nat.eq_zero_or_pos UInt256_max),
    exfalso,
    injection h,
  end

def literal_zero : Literal :=
  fin.mk 0 zero_lt_uint256_max

set_option class.instance_max_depth 100

def FTContext := Identifier → option (ℕ × ℕ)
def empΓ : FTContext := λ_, none

def VarStore (vars : finset Identifier) := Π i : Identifier, (i ∈ vars) → Literal
def empStore : VarStore ∅
  | i i_in_emp := absurd i_in_emp (finset.not_mem_empty i)

def tofinset' : ∀ (n : ℕ) (α : Type) [decidable_eq α], vector α n -> finset α
| 0 _ _ vec := ∅
| (nat.succ n) α hs_un vec :=
  let union := (@finset.has_union α hs_un).union
  in union (singleton (vec.head)) (@tofinset' n α hs_un (vec.tail))

def tofinset {n : ℕ} {α : Type} [α_eq_dec : decidable_eq α] (f : fin n → α) : finset α :=
      tofinset' n α (vector.of_fn f)

inductive TType : Type
| BlockList : FTContext → finset Identifier → finset Identifier → TType
| CBlock : FTContext → finset Identifier → TType
| SwitchBody : FTContext → finset Identifier → TType
| CExpr : FTContext → finset Identifier → ℕ → TType
| CStatement : FTContext → finset Identifier → finset Identifier → TType

open TType

inductive Yulℂ : TType → Type
| EmpCBlock : ∀ (Γ : FTContext) (vars : finset Identifier), Yulℂ (BlockList Γ vars vars)
| SeqCBlock  :
  ∀ (Γ : FTContext) (vars : finset Identifier) (vars' : finset Identifier) (vars'' : finset Identifier),
    Yulℂ (CStatement Γ vars vars') -> Yulℂ (BlockList Γ vars' vars'') → Yulℂ (BlockList Γ vars vars'')

| NestedScope : ∀ (Γ : FTContext) (vars inner_vars inner_vars' : finset Identifier),
    VarStore inner_vars → Yulℂ (BlockList Γ (inner_vars ∪ vars) (inner_vars' ∪ vars)) → Yulℂ (CBlock Γ vars)

| CCase : ∀ (Γ : FTContext) (vars : finset Identifier),
    Literal → Yulℂ (CBlock Γ vars) → Yulℂ (SwitchBody Γ vars) → Yulℂ (SwitchBody Γ vars)
| CDefault : ∀ (Γ : FTContext) (vars : finset Identifier),
    Yulℂ (CBlock Γ vars) → Yulℂ (SwitchBody Γ vars)

| CFunctionCall : ∀ (Γ : FTContext) (vars : finset Identifier)
                    (f_id : Identifier) (n : ℕ) (m : ℕ),
    (Γ f_id = some (n,m)) →
    (fin n → Yulℂ (CExpr Γ vars 1)) →
    Yulℂ (CExpr Γ vars m)
| CId : ∀ (Γ : FTContext) (vars : finset Identifier) (id : Identifier), id ∈ vars → Yulℂ (CExpr Γ vars 1)
| CLit : ∀ (Γ : FTContext) (vars : finset Identifier), Literal → Yulℂ (CExpr Γ vars 1)
| Scope : ∀ (Γ : FTContext) (vars_outer vars_inner vars_inner' : finset Identifier)
               (m : ℕ) (ret_vars : fin m → Identifier),
    VarStore (vars_inner ∪ (tofinset ret_vars)) →
    Yulℂ (CStatement Γ (vars_inner ∪ (tofinset ret_vars)) (vars_inner' ∪ (tofinset ret_vars))) →
    Yulℂ (CExpr Γ vars_outer m)

| CBlock : ∀ (Γ : FTContext) (vars : finset Identifier), Yulℂ (CBlock Γ vars) → Yulℂ (CStatement Γ vars vars)
  -- Function definitions already parsed into FTContext.
| CVariableDeclarationAss :
    ∀ (Γ : FTContext) (vars : finset Identifier) (n : ℕ) (new_vars : fin n -> Identifier),
      Yulℂ (CExpr Γ vars n) →  Yulℂ (CStatement Γ vars (vars ∪ (tofinset new_vars)))
| CVariableDeclaration :
    ∀ (Γ : FTContext) (vars : finset Identifier) (n : ℕ) (new_vars : fin n -> Identifier),
      Yulℂ (CStatement Γ vars (vars ∪ (tofinset new_vars)))
| CAssignment : ∀ (Γ : FTContext) (vars : finset Identifier) (n : ℕ) (ids : fin n -> Identifier),
    tofinset ids ⊆ vars → Yulℂ (CExpr Γ vars n) → Yulℂ (CStatement Γ vars vars)
| CIf : ∀ (Γ : FTContext) (vars : finset Identifier),
    Yulℂ (CExpr Γ vars 1) → Yulℂ (CBlock Γ vars) → Yulℂ (CStatement Γ vars vars)
| CExpressionStatement : ∀ (Γ : FTContext) (vars : finset Identifier),
    Yulℂ (CExpr Γ vars 0) -> Yulℂ (CStatement Γ vars vars)
| CSwitch : ∀ (Γ : FTContext) (vars : finset Identifier),
    Yulℂ (CExpr Γ vars 1) →
    Yulℂ (SwitchBody Γ vars) →
    Yulℂ (CStatement Γ vars vars)
| CFor : ∀ (Γ : FTContext) (vars vars' vars'' vars''' : finset Identifier),
    Yulℂ (BlockList Γ vars vars') → Yulℂ (CExpr Γ vars' 1) →
    Yulℂ (BlockList Γ vars' vars'') → Yulℂ (BlockList Γ vars'' vars''') →
    Yulℂ (CStatement Γ vars vars)
| CBreak : ∀ (Γ : FTContext) (vars : finset Identifier), Yulℂ (CStatement Γ vars vars)
| CContinue : ∀ (Γ : FTContext) (vars : finset Identifier), Yulℂ (CStatement Γ vars vars)
| CLeave : ∀ (Γ : FTContext) (vars : finset Identifier), Yulℂ (CStatement Γ vars vars)
| ForCheckCond : ∀ (Γ : FTContext) (vars : finset Identifier),
    Yulℂ (CExpr Γ vars 1) → Yulℂ (BlockList Γ vars vars) -> Yulℂ (CExpr Γ vars 1) ->
    Yulℂ (CStatement Γ vars vars)
| ForExecBody : ∀ (Γ : FTContext) (vars : finset Identifier),
    Yulℂ (CExpr Γ vars 1) → Yulℂ (BlockList Γ vars vars) →
    Yulℂ (CStatement Γ vars vars) -> Yulℂ (CStatement Γ vars vars)
| Skip : ∀ (Γ : FTContext) (vars : finset Identifier), Yulℂ (CStatement Γ vars vars)
  -- ForCheckCond, ForExecbody and Skip not in Yul specification, added for small step semantics.

open Yulℂ

def is_skip : ∀ {Γ : FTContext} {vars vars': finset Identifier}, Yulℂ (CStatement Γ vars vars') -> Prop
| _ _ _ (Skip _ _) := true
| _ _ _ (CBlock _ _ _) := false
| _ _ _ (CVariableDeclarationAss _ _ _ _ _) := false
| _ _ _ (CVariableDeclaration _ _ _ _) := false
| _ _ _ (CAssignment _ _ _ _ _ _) := false
| _ _ _ (CIf _ _ _ _) := false
| _ _ _ (CExpressionStatement _ _ _) := false
| _ _ _ (CSwitch _ _ _ _) := false
| _ _ _ (CFor _ _ _ _ _ _ _ _ _) := false
| _ _ _ (CBreak _ _) := false
| _ _ _ (CContinue _ _) := false
| _ _ _ (CLeave _ _) := false
| _ _ _ (ForCheckCond _ _ _ _ _) := false
| _ _ _ (ForExecBody _ _ _ _ _) := false

def is_evaluated : ∀ {t : TType}, Yulℂ t → Prop
| (BlockList _ _ _) (EmpCBlock _ _) := true
| (BlockList _ _ _) _               := false
| (CBlock _ _) (NestedScope _ _ _ _ _ blklst) := is_evaluated blklst
| (SwitchBody _ _) _ := false
| (CExpr _ _ _) (CLit _ _ _) := true
| (CExpr _ _ _) (CId _ _ _ _) := false
| (CExpr _ _ n) (Scope _ _ _ _ _ _ _ cstmnt) := (n ≠ 1) ∧ is_skip cstmnt
| (CExpr _ _ _) _ := false
| (CStatement _ _ _) cstmnt := is_skip cstmnt
| (CStatement _ (@finset.mk.{0} Identifier _ _) (@finset.mk.{0} Identifier _ _)) _ := false

[Chris B]

I'm getting a segfault on the recursive case, but this doesn't show any errors for me:

def is_evaluated : ∀ {t : TType}, Yulℂ t → Prop
| (BlockList _ _ _) (EmpCBlock _ _) := true
| (BlockList _ _ _) _               := false
--| (CBlock _ _) (NestedScope _ _ _ _ _ blklst) := is_evaluated blklst
| (CBlock _ _) _ := true
| (SwitchBody _ _) _ := false
| (CExpr _ _ _) (CLit _ _ _) := true
| (CExpr _ _ _) (CId _ _ _ _) := false
| (CExpr _ _ n) (Scope _ _ _ _ _ _ _ cstmnt) := (n ≠ 1) ∧ is_skip cstmnt
| (CExpr _ _ _) _ := false
| (CStatement _ _ _) cstmnt := is_skip cstmnt

The dependent match for the NestedScope case shouldn't work as written anyway since blklst isn't going to be the same as t. That said the segfault is a mystery. I'm on 3.24 which is old-ish, so it may be fixed in newer versions.

[Julian Sutherland]

I'm on 3.34 myself. Will try and see if this works with a more recent version of lean 3 :)

I'm not sure I follow you? The recursive call to is_evaluated is well-typed. As you point out, lean will infer a different value of t, the implicit argument, but I don't see why that would be a problem?

[Chris B]

The inference wasn't working in 3.24, I'm sure they just improved the dependent pattern matching in the interim. I'm trying it on 3.35.1 and getting the same error you are. I think this might just a bug in the dependent pattern matching that's somehow caused by the NestedScope case.

[Julian Sutherland]

You're right, it seems to be the case that this recursive case is causing the problem. I guess I can get around this by explicitly matching on the EmpCBlock constructor in the CBlock case. Will give it a try.

Re: this potential bug, I will try and generate a #mwe, would it be best to raise this as an issue on GitHub?

[Julian Sutherland]

Hmmm, no success, I tried

def is_evaluated : ∀ {t : TType}, Yulℂ t → Prop
| (BlockList _ _ _) (EmpCBlock _ _) := true
| (BlockList _ _ _) _               := false
| (CBlock _ _) (NestedScope _ _ _ _ _ (EmpCBlock _ _)) := true
| (CBlock _ _) (NestedScope _ _ _ _ _ _) := false
| (SwitchBody _ _) _ := false
| (CExpr _ _ _) (CLit _ _ _) := true
| (CExpr _ _ _) (CId _ _ _ _) := false
| (CExpr _ _ n) (Scope _ _ _ _ _ _ _ cstmnt) := (n ≠ 1) ∧ is_skip cstmnt
| (CExpr _ _ _) _ := false
| (CStatement _ _ _) cstmnt := is_skip cstmnt

and got

equation compiler failed (use 'set_option trace.eqn_compiler.elim_match true' for additional details)
nested exception message:
cases tactic failed, unsupported equality between type and constructor indices
(only equalities between constructors and/or variables are supported, try cases on the indices):
quot.lift
    (λ (a₁ : list Identifier),
       quotient.lift ((λ (l₁ l₂ : list Identifier), ↑(l₁.union l₂)) a₁) _ t_ᾰ_1.val)
    _
    ᾰ_inner_vars'.val =
  quot.lift
    (λ (a₁ : list Identifier),
       quotient.lift ((λ (l₁ l₂ : list Identifier), ↑(l₁.union l₂)) a₁) _ t_ᾰ_1.val)
    _
    ᾰ_inner_vars.val

I tried setting set_option trace.eqn_compiler.elim_match true and the resulting message is gigantic...

[Chris B]

Yeah, the leanprover-community lean3 repo still handles issues and PRs.

[Julian Sutherland]

Super, will give that a try! :)

[Julian Sutherland]

Was able to get it working by defining an auxiliary function:

def is_empcblock :
  ∀ {Γ : FTContext} {vars vars' : finset Identifier}, Yulℂ (BlockList Γ vars vars') → Prop
| _ _ _ (EmpCBlock _ _) := true
| _ _ _ _ := false

def is_evaluated : ∀ {t : TType}, Yulℂ t → Prop
| (BlockList _ _ _) blklst := is_empcblock blklst
| (CBlock _ _) (NestedScope _ _ _ _ _ blklst) := is_empcblock blklst
| (SwitchBody _ _) _ := false
| (CExpr _ _ _) (CLit _ _ _) := true
| (CExpr _ _ _) (CId _ _ _ _) := false
| (CExpr _ _ n) (Scope _ _ _ _ _ _ _ cstmnt) := (n ≠ 1) ∧ is_skip cstmnt
| (CExpr _ _ _) _ := false
| (CStatement _ _ _) cstmnt := is_skip cstmnt

Nonetheless, I will try and generate an #mwe as soon possible, as I see no reason the original should not have worked.

@Chris B Thanks so much for all your help :)

[Huỳnh Trần Khanh]

Julian Sutherland said:

Huỳnh Trần Khanh I gave that a try, while it works, the generated equations are extremely large and quite difficult to use practically in proofs it seems... Thanks :)

for the record, there is a way to make the generated equations easier to deal with. you should prove lemmas that correspond to the cases that you normally state while pattern matching and to prove these lemmas, you can use squeeze_simp and possibly some induction and for the most part, lean can simplify the humongous expression on its own. take a look at this tiny example:

import tactic

def sum_of_1_to_n : ℕ → ℕ := begin
  intro n,
  induction n,
  exact 0,
  exact n_n + n_ih,
end

lemma base_case : sum_of_1_to_n 0 = 0 := begin
  simp only [sum_of_1_to_n, nat.rec_zero], -- generated by squeeze_simp
end

lemma induction_hypothesis : ∀ n, sum_of_1_to_n (n + 1) = sum_of_1_to_n n + n := begin
  intro n,
  induction n,
  simp only [sum_of_1_to_n, nat.rec_add_one], -- generated by squeeze_simp
  simp only [sum_of_1_to_n, nat.rec_add_one], -- generated by squeeze_simp
  ring,
end

squeeze_simp is quite helpful actually

[Huỳnh Trần Khanh]

and here's a nontrivial example

import tactic

inductive word_size_t
| char
| i32
| i64

inductive integer_expression_t : word_size_t → Type
| const { word_size : word_size_t } (value : ℤ) : integer_expression_t word_size
| coerce { word_size word_size' : word_size_t } (a : integer_expression_t word_size') : integer_expression_t word_size
| load { word_size : word_size_t } (index : integer_expression_t word_size_t.i32) : integer_expression_t word_size
| add { word_size : word_size_t } (a b : integer_expression_t word_size) : integer_expression_t word_size
| subtract { word_size : word_size_t } (a b : integer_expression_t word_size) : integer_expression_t word_size
| multiply { word_size : word_size_t } (a b : integer_expression_t word_size) : integer_expression_t word_size
| divide { word_size : word_size_t } (a b : integer_expression_t word_size) : integer_expression_t word_size
| mod { word_size : word_size_t } (a b : integer_expression_t word_size) : integer_expression_t word_size
| bitwise_and { word_size : word_size_t } (a b : integer_expression_t word_size) : integer_expression_t word_size
| bitwise_or { word_size : word_size_t } (a b : integer_expression_t word_size) : integer_expression_t word_size
| bitwise_xor { word_size : word_size_t } (a b : integer_expression_t word_size) : integer_expression_t word_size
| bitwise_not { word_size : word_size_t } (a : integer_expression_t word_size) : integer_expression_t word_size

def evaluate : ∀ { word_size : word_size_t }, integer_expression_t word_size → ℕ := begin
  intros _ x,
  induction x,
  exact 1,
  exact x_ih + 1,
  exact x_ih + 1,
  exact x_ih_a + x_ih_b + 1,
  exact x_ih_a + x_ih_b + 1,
  exact x_ih_a + x_ih_b + 1,
  exact x_ih_a + x_ih_b + 1,
  exact x_ih_a + x_ih_b + 1,
  exact x_ih_a + x_ih_b + 1,
  exact x_ih_a + x_ih_b + 1,
  exact x_ih_a + x_ih_b + 1,
  exact x_ih + 1,
end

lemma a1 : ∀ word_size x, evaluate (@integer_expression_t.const word_size x) = 1 := begin
  intros,
  simp only [evaluate],
end

lemma a2 : ∀ word_size word_size' x, evaluate (@integer_expression_t.coerce word_size word_size' x) = evaluate x + 1 := begin
  intros,
  induction x,
  repeat {
    simp only [evaluate],
  },
end

lemma a3 : ∀ word_size x, evaluate (@integer_expression_t.load word_size x) = evaluate x + 1 := begin
  intros,
  simp only [evaluate],
end

lemma a4 : ∀ word_size x y, evaluate (@integer_expression_t.add word_size x y) = evaluate x + evaluate y + 1 := begin
  intros,
  simp only [evaluate],
end

lemma a5 : ∀ word_size x y, evaluate (@integer_expression_t.subtract word_size x y) = evaluate x + evaluate y + 1 := begin
  intros,
  simp only [evaluate],
end

lemma a6 : ∀ word_size x y, evaluate (@integer_expression_t.multiply word_size x y) = evaluate x + evaluate y + 1 := begin
  intros,
  simp only [evaluate],
end

lemma a7 : ∀ word_size x y, evaluate (@integer_expression_t.divide word_size x y) = evaluate x + evaluate y + 1 := begin
  intros,
  simp only [evaluate],
end

lemma a8 : ∀ word_size x y, evaluate (@integer_expression_t.mod word_size x y) = evaluate x + evaluate y + 1 := begin
  intros,
  simp only [evaluate],
end

lemma a9 : ∀ word_size x y, evaluate (@integer_expression_t.bitwise_and word_size x y) = evaluate x + evaluate y + 1 := begin
  intros,
  simp only [evaluate],
end

lemma a10 : ∀ word_size x y, evaluate (@integer_expression_t.bitwise_or word_size x y) = evaluate x + evaluate y + 1 := begin
  intros,
  simp only [evaluate],
end

lemma a11 : ∀ word_size x y, evaluate (@integer_expression_t.bitwise_xor word_size x y) = evaluate x + evaluate y + 1 := begin
  intros,
  simp only [evaluate],
end

lemma a12 : ∀ word_size x, evaluate (@integer_expression_t.bitwise_not word_size x) = evaluate x + 1 := begin
  intros,
  simp only [evaluate],
end

[Huỳnh Trần Khanh]

you should do this whenever the equation compiler acts up