struggling with a proof

Stream: lean4

[Arthur Paulino]

I'm trying to clear out this sorry but I'm having two problems:

• I'm not being able to use induction on l because Lean is complaining about a "type mismatch when assigning motive"
• Even if I succeeded at using induction, I'm afraid I wouldn't be able to go much further because I don't see a reference to consume in the context:

ctx : Context
n : String
es : NEList Expression
ns : NEList String
h : NEList.noDup ns = true
p✝ : Program
l? : Option (NEList String)
p : Program
hs : Option.isSome l? = true
l : NEList String := Option.get l? hs
⊢ NEList.noDup l = true

consume is a function that consumes an NEList. So what I'm trying to prove is basically that if the initial NEList doesn't have duplicated values, then the resulting NEList won't either.

[Leonardo de Moura]

Disclaimer: I did not download/try your example on my machine. So, take the following suggestion with a grain of salt :)
The notation

        let (l?, p) := consume p ns es
        <rest>

is syntax sugar for

match consume p ns es with
| (l?, p) => <rest>

In the match-expression we can annotate discriminants to get a hypotheses stating they are equal to the pattern. Example:

match h : consume p ns es with
| (l?, p) => <rest>

If you use this annotation, we will have h : consume p ns es = (l?, p) in your local context.
We currently do not have a similar notation for the let syntax sugar above.

[Leonardo de Moura]

For the first issue, it seems to be a bug in the induction tactic when the variable is a let-declaration. I will take a look.
In the meantime, you can make progress by using let_fun instead

          let_fun l : NEList String := l?.get hs

let_fun x := v; b is sugar for (fun x => b) v

[Leonardo de Moura]

BTW, you can also simplify

if hs : l?.isSome then
          let l := l?.get hs
          have : l.noDup := sorry
          return curry l this p
        else
          return (← p.runIO ctx).2

to

match l? with
| some l =>
          have : l.noDup := sorry
          return curry l this p
 | none =>
          return (← p.runIO ctx).2

or

if let some l := l? then
          have : l.noDup := sorry
          return curry l this p
else
          return (← p.runIO ctx).2

[Leonardo de Moura]

You can also combine the consume match with the one above and write

        match h : consume p ns es with
        |  (some l, p) =>
            have : l.noDup := sorry
            curry l this p
        | _ => (p.run ctx).2

[Arthur Paulino]

Yeah that's precisely how it was before but I changed it as an attempt to get consume in my context

[Leonardo de Moura]

Note that, you will now have h : consume p ns es = ...

[Arthur Paulino]

Oh right! It's actually slightly different. Thanks!!

[Arthur Paulino]

I will try it when I get home

[Arthur Paulino]

Not sure if this is hard, or tricky, or if I'm simply not competent enough, but how would you prove this one?

theorem eqqIffEq [BEq α] {a b : α} : a == b ↔ a = b := sorry

[Mauricio Collares]

It's provable if you replace BEq by LawfulBEq, but you're out of luck if your BEq instance is not lawful.

[Arthur Paulino]

Thanks! I didn't know about LawfulBEq!

theorem eqIffBEq [BEq α] [LawfulBEq α] {a b : α} : a == b ↔ a = b := by
  constructor
  · intro h; exact eq_of_beq h
  · intro h; simp [h]

[Arthur Paulino]

Why is it that sometimes we end up with infeasible inductive hypotheses? Is it a symptom os flawed definitions? In this example I can't seem to be able to use hn without assuming something false:

inductive NEList (α : Type)
  | uno  : α → NEList α
  | cons : α → NEList α → NEList α

def NEList.contains [BEq α] : NEList α → α → Bool
  | uno a,     x => a == x
  | cons a as, x => a == x || as.contains x

def NEList.noDupAux [BEq α] (l : List α) : NEList α → Bool
  | .uno  a   => ¬ l.contains a
  | .cons a r => ¬ l.contains a && ¬ r.contains a && noDupAux (a :: l) r

def NEList.noDup [BEq α] (l : NEList α) : Bool :=
  noDupAux [] l

mutual

  inductive Value
    | nil   : Value
    | bool  : Bool        → Value
    | int   : Int         → Value
    | float : Float       → Value
    | list  : Array Value → Value
    | str   : String      → Value
    | error : String      → Value
    | curry : (l : NEList String) → l.noDup → Program → Value
    deriving Inhabited

  inductive Expression
    | atom : Value      → Expression
    | var  : String     → Expression
    | not  : Expression → Expression
    | app  : String     → NEList Expression → Expression
    | add  : Expression → Expression → Expression
    | mul  : Expression → Expression → Expression
    | eq   : Expression → Expression → Expression
    | ne   : Expression → Expression → Expression
    | lt   : Expression → Expression → Expression
    | le   : Expression → Expression → Expression
    | gt   : Expression → Expression → Expression
    | ge   : Expression → Expression → Expression

  inductive Program
    | skip        : Program
    | sequence    : Program    → Program → Program
    | attribution : String     → Program → Program
    | ifElse      : Expression → Program → Program → Program
    | whileLoop   : Expression → Program → Program
    | evaluation  : Expression → Program
    | fail        : String     → Program
    deriving Inhabited

end

open NEList Program in
def consume (p : Program) :
    NEList String → NEList Expression → (Option (NEList String)) × Program
  | cons n ns, cons e es =>
    consume (sequence (attribution n (evaluation e)) p) ns es
  | cons n ns, uno  e    => (some ns, sequence (attribution n (evaluation e)) p)
  | uno  n,    uno  e    => (none, sequence (attribution n (evaluation e)) p)
  | uno  _,    cons ..   => (none, fail "incompatible number of parameters")

theorem noDupOfNoDupAux {ns : NEList α} [BEq α] (h : NEList.noDupAux l ns) :
    ns.noDup := sorry -- this is fine

theorem noDupOfConsumeNoDup
  (h : NEList.noDup ns) (h' : consume p' ns es = (some l, p)) :
    NEList.noDup l = true := by
    induction ns with
    | uno n =>
      cases es with
      | _ => simp [consume] at h'
    | cons n ns hn =>
      simp [NEList.noDup, NEList.noDupAux] at h
      have hn := hn $ noDupOfNoDupAux h.2
      have : consume p' (NEList.cons n ns) es = consume p' ns es := by
        -- `(NEList.cons n ns)` can't be defeq to `ns`... not fine!
        sorry
      rw [this] at h'
      exact hn h'

Any ideas what I might be doing wrong?

[Mario Carneiro]

the issue is usually a missing generalizing on induction

[Arthur Paulino]

Thanks!!

[Mario Carneiro]

theorem noDupOfConsumeNoDup
  (h : NEList.noDup ns) (h' : consume p' ns es = (some l, p)) :
    NEList.noDup l = true := by
    induction ns generalizing p' es with
    | uno n => cases es <;> cases h'
    | cons n ns ih =>
      simp [NEList.noDup, NEList.noDupAux] at h
      have h := noDupOfNoDupAux h.2
      cases es with
      | uno e => cases h'; exact h
      | cons e es => exact ih h h'

[Arthur Paulino]

I have the impression that this should be simple, but I don't know what I'm missing

inductive Foo
  | foo : Nat → Foo
  | foos : Array Foo → Foo
  deriving BEq

example : Foo.foo 0 ≠ Foo.foo 1 := by simp
-- Goals accomplished 🎉

example : #[0] ≠ #[1] := by simp
-- Goals accomplished 🎉

example : #[Foo.foo 0] ≠ #[Foo.foo 1] := by simp
-- unsolved goals
-- ⊢ ¬#[Foo.foo 0] = #[Foo.foo 1]

example : Foo.foos #[.foo 0] ≠ Foo.foos #[.foo 1] := by simp
-- unsolved goals
-- ⊢ ¬#[Foo.foo 0] = #[Foo.foo 1]

Can someone help me please? :pray:

[Siddharth Bhat]

inductive Foo
  | foo : Nat → Foo
  | foos : Array Foo → Foo
  deriving BEq

example : Foo.foo 0 ≠ Foo.foo 1 := by simp
-- Goals accomplished 🎉

example : #[0] ≠ #[1] := by simp
-- Goals accomplished 🎉

example : #[Foo.foo 0] ≠ #[Foo.foo 1] := by {
  unfold Not;
  intros CONTRA;
  exact (nomatch CONTRA);
}
-- goals accomplished

example : Foo.foos #[.foo 0] ≠ Foo.foos #[.foo 1] :=
by {
  unfold Not;
  intros CONTRA;
  exact (nomatch CONTRA);
}
-- goals accomplished

[Siddharth Bhat]

I doubt this is the best way to write this in lean. I wrote it as I would in Coq, which is to unfold the Not, intros the absurd hypothesis, and then claim that the absurdity is vacuously true.

[Arthur Paulino]

Does your kernel accept it? Mine doesn't: leanprover/lean4:nightly-2022-05-18

[Siddharth Bhat]

I was on leanprover/lean4:nightly-2022-03-30. Let me try on a newer version.

[Siddharth Bhat]

inductive Foo
  | foo : Nat → Foo
  | foos : Array Foo → Foo
  deriving BEq

example : Foo.foo 0 ≠ Foo.foo 1 := by simp
-- Goals accomplished 🎉

example : #[0] ≠ #[1] := by simp
-- Goals accomplished 🎉

example : #[Foo.foo 0] ≠ #[Foo.foo 1] := fun CONTRA => nomatch CONTRA

example : Foo.foos #[.foo 0] ≠ Foo.foos #[.foo 1] := fun CONTRA => nomatch CONTRA

This formulation works on leanprover/lean4:nightly-2022-05-18

[Siddharth Bhat]

example : #[Foo.foo 0] ≠ #[Foo.foo 1] := by {
  intros CONTRA;
  exact (nomatch CONTRA);
}

in proof mode also works for me on Lean (version 4.0.0-nightly-2022-05-18, commit eb170d1f43e8, Release). Does it for you, @Arthur Paulino ?

[Arthur Paulino]

Yeah

example : #[Foo.foo 0] ≠ #[Foo.foo 1] := by
  intro h
  exact nomatch h

[Arthur Paulino]

Thanks!!

[Leonardo de Moura]

@Arthur Paulino Thanks for pointing it out. I added the missing simp theorem.

List.of_toArray_eq_toArray (as bs : List α) : (as.toArray = bs.toArray) = (as = bs) :=

All examples should now go through using by simp.