How to simplify this proof without using a have statement?

Stream: Is there code for X?

[Colin Jones ⚛️]

I have this proof about powersets and proper divisors for the number 70.

import Mathlib

open Nat
open Finset
open BigOperators

example : ∀ s ∈ Finset.powerset (Nat.properDivisors 70), ∑ i in s, i ≠ 70 := by
  rintro s hs
  have hp : properDivisors 70 = {1, 2, 5, 7, 10, 14, 35} := by exact rfl
  rw [hp] at hs
  sorry

#eval powerset (properDivisors 70)

Is it possible to proof without stating the output of the #eval in the theorem as a have statement?

[Colin Jones ⚛️]

Similar to how hp is defined, but I'd rather not do that for the powerset of properDivisors

[Eric Wieser]

This works:

theorem Finset.powerset_singleton (a : α) :
  Finset.powerset {a} = .cons (∅ : Finset α) {{a}} (fun h => singleton_ne_empty a <| Eq.symm <| by simpa [eq_comm] using h) := by
    rfl

example : ∀ s ∈ Finset.powerset (Nat.properDivisors 70), ∑ i in s, i ≠ 70 := by
  rintro s hs
  have hp : properDivisors 70 = {1, 2, 5, 7, 10, 14, 35} := by exact rfl
  rw [hp] at hs
  simp only [Finset.powerset_insert, Finset.powerset_singleton, image_union, Finset.cons_eq_insert, image_insert, image_singleton, insert_empty, insert_union, union_insert,
  ←insert_eq] at hs

[Colin Jones ⚛️]

Did you use simp? or aesop? to find that sequence?

[Eric Wieser]

No, I did it by looking at the goal and using apply? to find the lemmas I couldn't guess the names of

[Eric Wieser]

Here's a nasty hack that really uses eval:

import Mathlib

open Nat
open Finset

universe u

set_option autoImplicit false
open Qq


class HasInstance (α : Type u) where
  expr : Lean.Expr

instance : HasInstance (DecidableEq ℕ) := ⟨q(inferInstanceAs <| DecidableEq ℕ)⟩
instance : HasInstance (DecidableEq (Finset ℕ)) := ⟨q(inferInstanceAs <| DecidableEq  (Finset ℕ))⟩
instance : HasInstance (DecidableEq (Finset (Finset ℕ))) := ⟨q(inferInstanceAs <| DecidableEq  (Finset  (Finset ℕ)))⟩

open Qq Lean
unsafe instance foo {α : Type u} [ToLevel.{u}] [Lean.ToExpr α] [HasInstance (DecidableEq α)] : Lean.ToExpr (Finset α) :=
  have u' : Level := ToLevel.toLevel.{u}
  have α' : Q(Type u') := Lean.ToExpr.toTypeExpr α
  letI : Q(DecidableEq $α') := HasInstance.expr (DecidableEq α)
  { toTypeExpr := q(Finset $α')
    toExpr := fun x => show Q(Finset $α') from
      match x.val.unquot.reverse with
      | [] => q(∅)
      | x0 :: xs =>
        let x0' : Q($α') := toExpr x0;
        List.foldl (fun s x=> let x' : Q($α') := toExpr x; q(insert $x' $s)) q({$x0'} : Finset $α') xs }

open Qq
syntax (name := eval_expr) "eval% " term : term
@[term_elab eval_expr]
unsafe def elabExprElab : Lean.Elab.Term.TermElab
| `(term| eval% $stx) => fun exp => do
  let e ← Lean.Elab.Term.elabTermAndSynthesize stx exp
  let e ← instantiateMVars e
  let v ← Lean.Meta.evalExpr (Finset (Finset Nat)) q(Finset (Finset Nat)) e
  pure (Lean.toExpr v)
| _ => fun exp => throwError "nope"

open scoped BigOperators
example : ∀ s ∈ Finset.powerset (Nat.properDivisors 70), ∑ i in s, i ≠ 70 := by
  rintro s hs
  have hp : Finset.powerset (Nat.properDivisors 70) = eval% (Finset.powerset {1, 2, 5, 7, 10, 14, 35} : Finset (Finset Nat)) := by sorry
  sorry

[Eric Wieser]

Maybe @Kyle Miller can tell me a better way to write it

[Colin Jones ⚛️]

Wow that's really cool! I don't understand it but it works!

[Kevin Buzzard]

Trust me, most people don't understand that code...

[Colin Jones ⚛️]

So I proved the sorry after the hp in hp2, but how do I go through each s \in powerset (Nat.properDivisors 70 to show that the sum over s doesn't equal 70?

For example if I had s \in {1,2,3} with a goal such as \forall s \in {1,2,3}, s\= 4, what tactic would I use?

I tried cases and rcases but they both reduce the set into a list and a jumbled mess of computer science stuff.

Here is what I have so far expanding off of Eric Wieser.

import Mathlib

open Nat
open Finset

universe u
set_option maxRecDepth 1000000000000
set_option autoImplicit false
open Qq


class HasInstance (α : Type u) where
  expr : Lean.Expr

instance : HasInstance (DecidableEq ℕ) := ⟨q(inferInstanceAs <| DecidableEq ℕ)⟩
instance : HasInstance (DecidableEq (Finset ℕ)) := ⟨q(inferInstanceAs <| DecidableEq  (Finset ℕ))⟩
instance : HasInstance (DecidableEq (Finset (Finset ℕ))) := ⟨q(inferInstanceAs <| DecidableEq  (Finset  (Finset ℕ)))⟩

open Qq Lean
unsafe instance foo {α : Type u} [ToLevel.{u}] [Lean.ToExpr α] [HasInstance (DecidableEq α)] : Lean.ToExpr (Finset α) :=
  have u' : Level := ToLevel.toLevel.{u}
  have α' : Q(Type u') := Lean.ToExpr.toTypeExpr α
  letI : Q(DecidableEq $α') := HasInstance.expr (DecidableEq α)
  { toTypeExpr := q(Finset $α')
    toExpr := fun x => show Q(Finset $α') from
      match x.val.unquot.reverse with
      | [] => q(∅)
      | x0 :: xs =>
        let x0' : Q($α') := toExpr x0;
        List.foldl (fun s x=> let x' : Q($α') := toExpr x; q(insert $x' $s)) q({$x0'} : Finset $α') xs }

open Qq
syntax (name := eval_expr) "eval% " term : term
@[term_elab eval_expr]
unsafe def elabExprElab : Lean.Elab.Term.TermElab
| `(term| eval% $stx) => fun exp => do
  let e ← Lean.Elab.Term.elabTermAndSynthesize stx exp
  let e ← instantiateMVars e
  let v ← Lean.Meta.evalExpr (Finset (Finset Nat)) q(Finset (Finset Nat)) e
  pure (Lean.toExpr v)
| _ => fun exp => throwError "nope"

open scoped BigOperators
example : ∀ s ∈ Finset.powerset (Nat.properDivisors 70), ∑ i in s, i ≠ 70 := by
  rintro s hs
  have hp1 : Nat.properDivisors 70 = {1, 2, 5, 7, 10, 14, 35} := by exact rfl
  have hp2 : Finset.powerset (Nat.properDivisors 70) = eval% (Finset.powerset {1, 2, 5, 7, 10, 14, 35} : Finset (Finset Nat)) := by
    rw [hp1]
    exact rfl
  sorry

[Kyle Miller]

set_option maxRecDepth 2000 in
example : ∀ s ∈ Finset.powerset (Nat.properDivisors 70), ∑ i in s, i ≠ 70 := by
  rintro s hs
  fin_cases hs <;> decide

[Kyle Miller]

fin_cases operates by reduction instead of using eval. It does cases for you in a controlled way.

[Kyle Miller]

(Eric's idea makes me wonder if there should be an eval tactic that tries to simplify by evaluation and then post-hoc come up with a proof? Not sure how that would work though, since if you can only find the value by evaluation, without extra cleverness, like what norm_num provides, I'm not sure what you could do reduction couldn't, except maybe create nicer normal forms, like what Eric generated.)

[Colin Jones ⚛️]

Kyle Miller said:

(Eric's idea makes me wonder if there should be an eval tactic that tries to simplify by evaluation and then post-hoc come up with a proof? Not sure how that would work though, since if you can only find the value by evaluation, without extra cleverness, like what norm_num provides, I'm not sure what you could do reduction couldn't, except maybe create nicer normal forms, like what Eric generated.)

That's is what I was hoping for. Something where I could prove s ∈ {1,2,3} → powerset s = {∅, {1}, {2}, {3}, {1,2}, {2,3}, {1,3}, {1,2,3}} using a #eval kind of tactic.

[Eric Wieser]

Note that that tactics that use eval aren't actually very useful, as your example stops working as soon as you generalize away from Nat to a, b, c

[Eric Wieser]

I'm out of time for now, but I think the solution to my reflection issues above is to... add another layer of code generation

[Kyle Miller]

There could still be "norm_num for collections", among other sorts of evaluators. (I'm curious what the tactic landscape is going to look like now that we have simprocs.)

[Eric Wieser]

Here's a better version of eval%that doesn't hardcode Finset (Finest Nat):

@[term_elab eval_expr]
unsafe def elabExprElab : Lean.Elab.Term.TermElab
| `(term| eval% $stx) => fun exp => do
  let e ← Lean.Elab.Term.elabTermAndSynthesize stx exp
  let e ← instantiateMVars e
  let ee ← Elab.Term.elabTerm (← `(Lean.toExpr $(←e.toSyntax))) (some q(Expr))
  let v ← Lean.Meta.evalExpr Expr q(Expr) ee (safety := .unsafe)
  pure v
| _ => fun _ => Elab.throwUnsupportedSyntax

[Eric Wieser]

PR'd as #10742

[Jz Pan]

Kyle Miller said:

There could still be "norm_num for collections", among other sorts of evaluators. (I'm curious what the tactic landscape is going to look like now that we have simprocs.)

I think you mean computer algebra system modules to Lean.

[Ma, Jia-Jun]

I am proposing a more flexible version of eval%, which can handle Finset and without hard coding using HasInstance.

import Mathlib
import Qq
import Lean


open Qq Lean Meta

class ToExprM (α : Type u) where
  toExprM : α → MetaM Expr
  toTypeExprM : MetaM Expr

instance [h:ToExpr α] : ToExprM α where
  toExprM := fun x => pure (toExpr x)
  toTypeExprM := pure (h.toTypeExpr)

open Lean.Meta

def  toExprAux {α : Type u} [ToLevel.{u}] [inst:ToExprM α]: List α  → MetaM Expr := fun x => do
  let type ← ToExprM.toTypeExprM α
  let finsettype ← mkAppM ``Finset #[type]
  logInfo m!"{← ppExpr type}"
  match x with
  | []    => pure <| mkAppN (.const ``Finset.empty [toLevel.{u}]) #[type]
  | [a]   => mkAppOptM ``Singleton.singleton #[none,finsettype,none,(←inst.toExprM a)]
  | a::as => mkAppM ``Insert.insert #[(←inst.toExprM a),(←toExprAux as)]



unsafe instance Finset.toExprM
    {α : Type u} [ToLevel.{u}] [ToExprM α] [DecidableEq α] : ToExprM (Finset α) where
  toTypeExprM := do
    let type ← ToExprM.toTypeExprM α
    mkAppM ``Finset #[type]
  toExprM := fun x => (toExprAux x.val.unquot)


syntax (name := eval_exprm) "evalm% " term : term

@[term_elab eval_exprm, inherit_doc eval_exprm]
unsafe def elabEvalExpr : Lean.Elab.Term.TermElab
| `(term| evalm% $stx) => fun exp => do
  let e ← Lean.Elab.Term.elabTermAndSynthesize stx exp
  let e ← instantiateMVars e
  logInfo m!"{← ppExpr e}"
  let type ← inferType e
  let type ← whnf type
  logInfo m!"{← ppExpr type}"
  let ee ← Meta.mkAppM ``ToExprM.toExprM #[e]
  let eetype ← inferType ee
  logInfo m!"{← ppExpr eetype}"
  let ee ← Lean.Meta.evalExpr (MetaM Expr) eetype ee (safety := .unsafe)
  --Lean.Meta.evalExpr Expr q(Expr) e (safety :=.unsafe)
  return (←ee)
| _ => fun _ => Elab.throwUnsupportedSyntax


section test
#check @Singleton.singleton (ℕ) (Finset ℕ) _ 1
#check ({1,2} : Finset ℕ)

#check evalm% ({} : Finset ℕ )
#check evalm% ({({2^10,1} : Finset ℕ),{2^3,2^5}}: Finset (Finset ℕ))

lemma a: ({2^10,1} : Finset ℕ) = evalm% ({2^10,1} : Finset ℕ):= by rfl

def twopowers (n : ℕ) : Finset ℕ := match n with
| 0 => {1}
| n+1 => {2^(n+1)} ∪ twopowers n

#eval twopowers 10

example (x : ℕ ): x∈ twopowers 10 → x=1 ∨ x %2 =0:= by
  intro hx
  have hh : twopowers 10 = evalm% twopowers 10 := by native_decide
  rw [hh] at hx
  fin_cases hx <;> simp


#check a

end test