Simplifications in proofs/type-checking not happening; wh...

Stream: lean4

[Leonardo de Moura]

@Siddhartha Gadgil We would be very grateful if you could create a self-contained example that exposes the issue you are experiencing.
https://leanprover-community.github.io/mwe.html

[Siddhartha Gadgil]

@Leonardo de Moura Thanks. I will work on it.

[Siddhartha Gadgil]

Am I correct that whnf for an (indexed) inductive type should give one of the constructors applied to arguments?

[Siddhartha Gadgil]

I am struggling to minimize the example though I have made many simplifications. It seems to be a depth of recursion with matching issue. Concretely, I have the following situation.

• A function solveSATreturns something with an example input which gives problems (in a sense that I elaborate later).
• solveSAT is recursive, in fact calls itself twice.
• If I define a function solveSATOuter by copying the code of solveSAT, so this calls solveSAT instead of itself with the same example input, what is returned is fine.
• If even one of the calls to solveSAT in solveSatOuter is replaced by a recursive call to solveSatOuter, the problems resurface.

Here by problems I mean two things.

• the type of a term is not simplified (which it was upto the nightly build on September 19, 2021).
• when computing whnf (as I sketched above) stuff crashes.

As far as I can see, there is no reason solveSAT and solveSATOuter should behave differently as far as the first issue goes at least.

I welcome any suggestions on how to further minimize (the source for the stuff mentioned above is https://github.com/siddhartha-gadgil/Saturn/blob/whnf-crash/Saturn/WhnfMwe2.lean).

I will also keep trying to minimize.

Thanks.

[Siddhartha Gadgil]

The apparent bug shows up in the following code (about 200 lines, no dependancies). As I comment, making a tiny change (replacing cls by clauses, in a context with the statement let cls := clauses) causes the error to disappear.

I am posting this below for feedback before posting an issue. This is with nigthtly version 2021-09-20 (and presumably all later ones)

import Lean.Meta
open Nat

structure ProvedSkip(n m: Nat) where
  result : Nat
  lt : m < n → result = m
  ge : n ≤ m → result = m + 1

def provedSkip (n m : Nat) : ProvedSkip n m :=
  if c : m < n then
    ⟨m, fun _ => rfl, fun hyp => False.elim (Nat.lt_irrefl m (Nat.lt_of_lt_of_le c hyp))⟩
  else
    ⟨m + 1, fun hyp => absurd hyp c, fun _ => rfl⟩

def skip: Nat → Nat → Nat :=
  fun n m => (provedSkip n m).result

theorem skip_below_eq(n m : Nat) : m < n → (skip n m = m) :=
  fun hyp => (provedSkip n m).lt hyp

theorem skip_above_eq(n m : Nat) : n ≤ m → (skip n m = m + 1) :=
  fun hyp => (provedSkip n m).ge hyp

theorem skip_not_below_eq(n m : Nat) : Not (m < n) → (skip n m = m + 1) :=
  fun hyp =>
    let lem : n ≤ m :=
      match Nat.lt_or_ge m n with
      | Or.inl lt => absurd lt hyp
      | Or.inr ge => ge
    skip_above_eq n m lem

theorem skip_lt: (k j: Nat) →  skip k j < j + 2 :=
    fun k j =>
      if c : j < k then
        let eqn := skip_below_eq k j c
        by
          rw [eqn]
          apply Nat.le_step
          apply Nat.le_refl
          done
      else
        let eqn := skip_not_below_eq k j c
        by
          rw [eqn]
          apply Nat.le_refl
          done

theorem skip_le_succ {n k j : Nat} : j < n → skip k j < n + 1 :=
   by
    intro hyp
    apply Nat.le_trans (skip_lt k j)
    apply Nat.succ_lt_succ
    exact hyp

def FinSeq (n: Nat) (α : Type) : Type := (k : Nat) → k < n → α

theorem witness_independent{α : Type}{n : Nat}(seq: FinSeq n α) :
    (i : Nat)→ (j : Nat) → (iw : i < n) → (jw : j < n) →
        (i = j) → seq i iw = seq j jw :=
        fun i j iw jw eqn =>
          match j, eqn, jw with
          | .(i), rfl, ijw =>
               rfl

namespace FinSeq
def init {α : Type}{n: Nat}(seq : FinSeq (n + 1) α): FinSeq n α :=
  fun k w =>
      seq k (Nat.le_step w)

def last{α : Type}{n: Nat}(seq : FinSeq (n + 1) α): α :=
  seq n (Nat.le_refl _)

def delete{α : Type}{n: Nat}(k : Nat) (kw : k < (n + 1)) (seq : FinSeq (n + 1) α): FinSeq n α :=
  fun j w =>
    seq (skip k j) (skip_le_succ w)

end FinSeq

inductive Vector (α : Type) : Nat → Type where
  | nil : Vector α zero
  | cons{n: Nat}(head: α) (tail: Vector  α n) : Vector α  (n + 1)

infixr:66 "+:" => Vector.cons

open Vector

def Vector.coords {α : Type}{n : Nat}(v: Vector α n) : FinSeq n α :=
  fun j jw =>
  match n, v, j, jw with
  | .(zero), nil, k, lt => nomatch lt
  | m + 1, cons head tail, zero, lt => head
  | m + 1, cons head tail, j + 1, w =>  tail.coords j (Nat.le_of_succ_le_succ w)

def seqVecAux {α: Type}{n m l: Nat}: (s : n + m = l) →
    (seq1 : FinSeq n α) → (accum : Vector α m) →
       Vector α l:=
    match n with
    | zero => fun s => fun _ => fun seq2 =>
      by
        have ss : l = m := by
          rw [← s]
          apply Nat.zero_add
          done
        have sf : Vector α l = Vector α m := by
          rw [ss]
        exact Eq.mpr sf seq2
        done
    | k + 1 => fun s seq1 seq2 =>
      let ss : k + (m + 1)  = l :=
        by
          rw [← s]
          rw [(Nat.add_comm m 1)]
          rw [(Nat.add_assoc k 1 m)]
          done
      seqVecAux ss (seq1.init) ((seq1.last) +: seq2)

def FinSeq.vec {α : Type}{n: Nat} : FinSeq n α  →  Vector α n :=
    fun seq => seqVecAux (Nat.add_zero n) seq Vector.nil

def Clause(n : Nat) : Type := Vector (Option Bool) n

def Valuation(n: Nat) : Type := Vector Bool n

inductive SatAnswer{dom n: Nat}(clauses : Vector (Clause n) dom) where
  | unsat : SatAnswer clauses
  | sat :  SatAnswer clauses

structure SimpleRestrictionClauses{dom n: Nat}
    (clauses: Vector (Clause (n + 1)) dom) where
  codom : Nat
  restClauses : Vector  (Clause n) codom

def prependRes{dom n: Nat}(branch: Bool)(focus: Nat)(focusLt : focus < n + 1)
    (clauses: Vector (Clause (n + 1)) dom):
        (rd : SimpleRestrictionClauses clauses) →
           (head : Clause (n + 1)) →
        SimpleRestrictionClauses (head +: clauses) :=
        fun rd  head =>
          if c : head.coords focus focusLt = some branch then
            ⟨rd.codom, rd.restClauses⟩
          else
            ⟨rd.codom + 1, (FinSeq.vec (FinSeq.delete focus focusLt head.coords)) +: rd.restClauses⟩

def restClauses{dom n: Nat}(branch: Bool)(focus: Nat)(focusLt : focus < n + 1)
        (clauses: Vector (Clause (n + 1)) dom) :
         SimpleRestrictionClauses clauses :=
            match dom, clauses with
            | 0, _ =>  ⟨0, Vector.nil⟩
            | m + 1, Vector.cons head clauses =>
                prependRes branch focus focusLt clauses
                            (restClauses branch focus focusLt clauses) head

def answerSAT{n dom : Nat}: (clauses : Vector (Clause n) dom) →  SatAnswer clauses :=
      match n with
      | zero =>
           match dom with
            | zero => fun cls => SatAnswer.sat
            | l + 1 => fun _ =>  SatAnswer.unsat
      | m + 1 =>
        fun clauses =>
        let cls := clauses
        let bd := zero_lt_succ m
        let rd  :=
            restClauses false zero bd clauses
        let subCls := rd.restClauses
        let subSol: SatAnswer subCls := answerSAT subCls
        match subSol with
        | SatAnswer.sat   =>
          SatAnswer.sat
        | SatAnswer.unsat  =>
            let rd := restClauses true zero bd cls -- replacing cls by clauses fixes this
            let subCls := rd.restClauses
            let subSol : SatAnswer subCls := answerSAT subCls
            match subSol with
            | SatAnswer.sat   =>
                SatAnswer.sat
            | SatAnswer.unsat   =>
                SatAnswer.unsat

open Lean.Meta
open Lean.Elab.Term

syntax (name:= nrmlform)"whnf!" term : term
@[termElab nrmlform] def normalformImpl : TermElab :=
  fun stx expectedType? =>
  match stx with
  | `(whnf! $s) =>
      do
        let t ← elabTerm s none
        let e ← whnf t
        return e
  | _ => Lean.Elab.throwIllFormedSyntax


def cls1 : Clause 2 := -- ¬P
  (some false) +: (none) +: Vector.nil

def cls2 : Clause 2 := (some true) +: none +: Vector.nil  -- P

def egStatement := cls1 +: cls2 +: Vector.nil

def egAnswer : SatAnswer egStatement := answerSAT egStatement

def egAnswerNorm : SatAnswer egStatement := whnf! egAnswer                    -- gives the error

Thanks

[Leonardo de Moura]

@Siddhartha Gadgil Thanks for creating a self-contained repro. I just pushed a fix for this issue.

[Siddhartha Gadgil]

Wow, thanks a lot