Skip to content

Commit 37eb068

Browse files
kim-emChrisHughes24
kim-em
and
ChrisHughes24
authored
feat: a solution to if-normalization (#8035)
* feat: a solution to if-normalization * lint * import all * duplicated names * Update Archive/Examples/IfNormalization/Statement.lean Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com> * resist the temptation to let aesop specify the data * typo in doc-string * workaround * fix * fix * fix --------- Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
1 parent cdd069a commit 37eb068

File tree

4 files changed

+362
-0
lines changed

4 files changed

+362
-0
lines changed

‎Archive.lean‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,7 @@
11
import Archive.Arithcc
2+
import Archive.Examples.IfNormalization.Result
3+
import Archive.Examples.IfNormalization.Statement
4+
import Archive.Examples.IfNormalization.WithoutAesop
25
import Archive.Examples.MersennePrimes
36
import Archive.Examples.PropEncodable
47
import Archive.Imo.Imo1959Q1

‎Archive/Examples/IfNormalization/Result.lean‎

Lines changed: 121 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,121 @@
1+
/-
2+
Copyright (c) 2023 Chris Hughes. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Chris Hughes
5+
-/
6+
import Archive.Examples.IfNormalization.Statement
7+
import Mathlib.Data.List.AList
8+
import Mathlib.Tactic.Recall
9+
10+
/-!
11+
# A solution to the if normalization challenge in Lean.
12+
13+
See `Statement.lean` for background.
14+
-/
15+
16+
set_option autoImplicit true
17+
18+
macro "◾" : tactic => `(tactic| aesop)
19+
macro "◾" : term => `(term| by aesop)
20+
21+
namespace IfExpr
22+
23+
/-!
24+
We add some local simp lemmas so we can unfold the definitions of the normalization condition.
25+
-/
26+
attribute [local simp] normalized hasNestedIf hasConstantIf hasRedundantIf disjoint vars
27+
List.disjoint
28+
29+
/-!
30+
Adding these lemmas to the simp set allows Lean to handle the termination proof automatically.
31+
-/
32+
attribute [local simp] Nat.lt_add_one_iff le_add_of_le_right
33+
34+
/-!
35+
Some further simp lemmas for handling if-then-else statements.
36+
-/
37+
attribute [local simp] apply_ite ite_eq_iff'
38+
39+
-- A copy of Lean's `decide_eq_true_eq` which unifies the `Decidable` instance
40+
-- rather than finding it by typeclass search.
41+
-- See https://github.com/leanprover/lean4/pull/2816
42+
@[simp] theorem decide_eq_true_eq {i : Decidable p} : (@decide p i = true) = p :=
43+
_root_.decide_eq_true_eq
44+
45+
46+
/-!
47+
Simp lemmas for `eval`.
48+
We don't want a `simp` lemma for `(ite i t e).eval` in general, only once we know the shape of `i`.
49+
-/
50+
@[simp] theorem eval_lit : (lit b).eval f = b := rfl
51+
@[simp] theorem eval_var : (var i).eval f = f i := rfl
52+
@[simp] theorem eval_ite_lit :
53+
(ite (.lit b) t e).eval f = bif b then t.eval f else e.eval f := rfl
54+
@[simp] theorem eval_ite_var :
55+
(ite (.var i) t e).eval f = bif f i then t.eval f else e.eval f := rfl
56+
@[simp] theorem eval_ite_ite :
57+
(ite (ite a b c) d e).eval f = (ite a (ite b d e) (ite c d e)).eval f := by
58+
cases h : eval f a <;> simp_all [eval]
59+
60+
/-- Custom size function for if-expressions, used for proving termination. -/
61+
@[simp] def normSize : IfExpr → Nat
62+
| lit _ => 0
63+
| var _ => 1
64+
| .ite i t e => 2 * normSize i + max (normSize t) (normSize e) + 1
65+
66+
/-- Normalizes the expression at the same time as assigning all variables in
67+
`e` to the literal booleans given by `l` -/
68+
def normalize (l : AList (fun _ : ℕ => Bool)) :
69+
(e : IfExpr) → { e' : IfExpr //
70+
(∀ f, e'.eval f = e.eval (fun w => (l.lookup w).elim (f w) (fun b => b)))
71+
∧ e'.normalized
72+
∧ ∀ (v : ℕ), v ∈ vars e' → l.lookup v = none }
73+
| lit b => ⟨lit b, ◾⟩
74+
| var v =>
75+
match h : l.lookup v with
76+
| none => ⟨var v, ◾⟩
77+
| some b => ⟨lit b, ◾⟩
78+
| .ite (lit true) t e => have t' := normalize l t; ⟨t'.1, ◾⟩
79+
| .ite (lit false) t e => have e' := normalize l e; ⟨e'.1, ◾⟩
80+
| .ite (.ite a b c) t e => have i' := normalize l (.ite a (.ite b t e) (.ite c t e)); ⟨i'.1, ◾⟩
81+
| .ite (var v) t e =>
82+
match h : l.lookup v with
83+
| none =>
84+
have ⟨t', ht₁, ht₂, ht₃⟩ := normalize (l.insert v true) t
85+
have ⟨e', he₁, he₂, he₃⟩ := normalize (l.insert v false) e
86+
⟨if t' = e' then t' else .ite (var v) t' e', by
87+
refine ⟨fun f => ?_, ?_, fun w b => ?_⟩
88+
· -- eval = eval
89+
simp
90+
cases hfv : f v
91+
· simp_all
92+
congr
93+
ext w
94+
by_cases w = v <;> ◾
95+
· simp [h, ht₁]
96+
congr
97+
ext w
98+
by_cases w = v <;> ◾
99+
· -- normalized
100+
have := ht₃ v
101+
have := he₃ v
102+
◾
103+
· -- lookup = none
104+
have := ht₃ w
105+
have := he₃ w
106+
by_cases w = v <;> ◾⟩
107+
| some b =>
108+
have i' := normalize l (.ite (lit b) t e); ⟨i'.1, ◾⟩
109+
termination_by normalize e => e.normSize
110+
111+
/-
112+
We recall the statement of the if-normalization problem.
113+
114+
We want a function from if-expressions to if-expressions,
115+
that outputs normalized if-expressions and preserves meaning.
116+
-/
117+
recall IfNormalization :=
118+
{ Z : IfExpr → IfExpr // ∀ e, (Z e).normalized ∧ (Z e).eval = e.eval }
119+
120+
example : IfNormalization :=
121+
⟨_, fun e => ⟨(IfExpr.normalize ∅ e).2.2.1, by simp [(IfExpr.normalize ∅ e).2.1]⟩⟩

‎Archive/Examples/IfNormalization/Statement.lean‎

Lines changed: 107 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,107 @@
1+
/-
2+
Copyright (c) 2023 Lean FRO LLC. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Scott Morrison
5+
-/
6+
7+
/-!
8+
# If normalization
9+
10+
Rustan Leino, Stephan Merz, and Natarajan Shankar have recently been discussing challenge problems
11+
to compare proof assistants.
12+
(See https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Rustan's.20challenge)
13+
14+
Their first suggestion was "if-normalization".
15+
16+
This file contains a Lean formulation of the problem. See `Result.lean` for a Lean solution.
17+
-/
18+
19+
/-- An if-expression is either boolean literal, a numbered variable,
20+
or an if-then-else expression where each subexpression is an if-expression. -/
21+
inductive IfExpr
22+
| lit : Bool → IfExpr
23+
| var : Nat → IfExpr
24+
| ite : IfExpr → IfExpr → IfExpr → IfExpr
25+
deriving DecidableEq, Repr
26+
27+
namespace IfExpr
28+
29+
/--
30+
An if-expression has a "nested if" if it contains
31+
an if-then-else where the "if" is itself an if-then-else.
32+
-/
33+
def hasNestedIf : IfExpr → Bool
34+
| lit _ => false
35+
| var _ => false
36+
| ite (ite _ _ _) _ _ => true
37+
| ite _ t e => t.hasNestedIf || e.hasNestedIf
38+
39+
/--
40+
An if-expression has a "constant if" if it contains
41+
an if-then-else where the "if" is itself a literal.
42+
-/
43+
def hasConstantIf : IfExpr → Bool
44+
| lit _ => false
45+
| var _ => false
46+
| ite (lit _) _ _ => true
47+
| ite i t e => i.hasConstantIf || t.hasConstantIf || e.hasConstantIf
48+
49+
/--
50+
An if-expression has a "redundant if" if it contains
51+
an if-then-else where the then and else clauses are identical.
52+
-/
53+
def hasRedundantIf : IfExpr → Bool
54+
| lit _ => false
55+
| var _ => false
56+
| ite i t e => t == e || i.hasRedundantIf || t.hasRedundantIf || e.hasRedundantIf
57+
58+
/--
59+
All the variables appearing in an if-expressions, read left to right, without removing duplicates.
60+
-/
61+
def vars : IfExpr → List Nat
62+
| lit _ => []
63+
| var i => [i]
64+
| ite i t e => i.vars ++ t.vars ++ e.vars
65+
66+
/--
67+
A helper function to specify that two lists are disjoint.
68+
-/
69+
def _root_.List.disjoint {α} [DecidableEq α] : List α → List α → Bool
70+
| [], _ => true
71+
| x::xs, ys => x ∉ ys && xs.disjoint ys
72+
73+
/--
74+
An if expression evaluates each variable at most once if for each if-then-else
75+
the variables in the if clause are disjoint from the variables in the then clause, and
76+
the variables in the if clause are disjoint from the variables in the else clause.
77+
-/
78+
def disjoint : IfExpr → Bool
79+
| lit _ => true
80+
| var _ => true
81+
| ite i t e =>
82+
i.vars.disjoint t.vars && i.vars.disjoint e.vars && i.disjoint && t.disjoint && e.disjoint
83+
84+
/--
85+
An if expression is "normalized" if it has not nested, constant, or redundant ifs,
86+
and it evaluates each variable at most once.
87+
-/
88+
def normalized (e : IfExpr) : Bool :=
89+
!e.hasNestedIf && !e.hasConstantIf && !e.hasRedundantIf && e.disjoint
90+
91+
/--
92+
The evaluation of an if expresssion at some assignment of variables.
93+
-/
94+
def eval (f : Nat → Bool) : IfExpr → Bool
95+
| lit b => b
96+
| var i => f i
97+
| ite i t e => bif i.eval f then t.eval f else e.eval f
98+
99+
end IfExpr
100+
101+
/--
102+
This is the statement of the if normalization problem.
103+
104+
We require a function from that transforms if expressions to normalized if expressions,
105+
preserving all evaluations.
106+
-/
107+
def IfNormalization : Type := { Z : IfExpr → IfExpr // ∀ e, (Z e).normalized ∧ (Z e).eval = e.eval }

‎Archive/Examples/IfNormalization/WithoutAesop.lean‎

Lines changed: 131 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,131 @@
1+
/-
2+
Copyright (c) 2023 Chris Hughes. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Chris Hughes, Scott Morrison
5+
-/
6+
import Archive.Examples.IfNormalization.Statement
7+
import Mathlib.Data.List.AList
8+
9+
/-!
10+
# A variant of Chris Hughes' solution for the if normalization challenge.
11+
12+
In this variant we eschew the use of `aesop`, and instead write out the proofs.
13+
14+
(In order to avoid duplicated names with `Result.lean`,
15+
we put primes on the declarations in the file.)
16+
-/
17+
18+
set_option autoImplicit true
19+
20+
namespace IfExpr
21+
22+
attribute [local simp] eval normalized hasNestedIf hasConstantIf hasRedundantIf disjoint vars
23+
List.disjoint max_add_add_right max_mul_mul_left Nat.lt_add_one_iff le_add_of_le_right
24+
25+
-- A copy of Lean's `decide_eq_true_eq` which unifies the `Decidable` instance
26+
-- rather than finding it by typeclass search.
27+
-- See https://github.com/leanprover/lean4/pull/2816
28+
@[simp] theorem decide_eq_true_eq' {i : Decidable p} : (@decide p i = true) = p :=
29+
_root_.decide_eq_true_eq
30+
31+
theorem eval_ite_ite' :
32+
(ite (ite a b c) d e).eval f = (ite a (ite b d e) (ite c d e)).eval f := by
33+
cases h : eval f a <;> simp_all
34+
35+
/-- Custom size function for if-expressions, used for proving termination. -/
36+
@[simp] def normSize' : IfExpr → ℕ
37+
| lit _ => 0
38+
| var _ => 1
39+
| .ite i t e => 2 * normSize' i + max (normSize' t) (normSize' e) + 1
40+
41+
/-- Normalizes the expression at the same time as assigning all variables in
42+
`e` to the literal booleans given by `l` -/
43+
def normalize' (l : AList (fun _ : ℕ => Bool)) :
44+
(e : IfExpr) → { e' : IfExpr //
45+
(∀ f, e'.eval f = e.eval (fun w => (l.lookup w).elim (f w) (fun b => b)))
46+
∧ e'.normalized
47+
∧ ∀ (v : ℕ), v ∈ vars e' → l.lookup v = none }
48+
| lit b => ⟨lit b, by simp⟩
49+
| var v =>
50+
match h : l.lookup v with
51+
| none => ⟨var v, by simp_all⟩
52+
| some b => ⟨lit b, by simp_all⟩
53+
| .ite (lit true) t e =>
54+
have ⟨t', ht'⟩ := normalize' l t
55+
⟨t', by simp_all⟩
56+
| .ite (lit false) t e =>
57+
have ⟨e', he'⟩ := normalize' l e
58+
⟨e', by simp_all⟩
59+
| .ite (.ite a b c) d e =>
60+
have ⟨t', ht₁, ht₂⟩ := normalize' l (.ite a (.ite b d e) (.ite c d e))
61+
⟨t', fun f => by rw [ht₁, eval_ite_ite'], ht₂⟩
62+
| .ite (var v) t e =>
63+
match h : l.lookup v with
64+
| none =>
65+
have ⟨t', ht₁, ht₂, ht₃⟩ := normalize' (l.insert v true) t
66+
have ⟨e', he₁, he₂, he₃⟩ := normalize' (l.insert v false) e
67+
⟨if t' = e' then t' else .ite (var v) t' e', by
68+
refine ⟨fun f => ?_, ?_, fun w b => ?_⟩
69+
· simp only [eval, apply_ite, ite_eq_iff']
70+
cases hfv : f v
71+
· simp (config := {contextual := true}) only [cond_false, h, he₁]
72+
refine ⟨fun _ => ?_, fun _ => ?_⟩
73+
· congr
74+
ext w
75+
by_cases w = v <;> rename_i x
76+
· substs h
77+
simp_all
78+
· simp_all
79+
· congr
80+
ext w
81+
by_cases w = v <;> rename_i x
82+
· substs h
83+
simp_all
84+
· simp_all
85+
· simp only [cond_true, h, ht₁]
86+
refine ⟨fun _ => ?_, fun _ => ?_⟩
87+
· congr
88+
ext w
89+
by_cases w = v <;> rename_i x
90+
· substs h
91+
simp_all
92+
· simp_all
93+
· congr
94+
ext w
95+
by_cases w = v <;> rename_i x
96+
· substs h
97+
simp_all
98+
· simp_all
99+
· have := ht₃ v
100+
have := he₃ v
101+
simp_all? says simp_all only [Option.elim, ne_eq, normalized, Bool.and_eq_true,
102+
Bool.not_eq_true', AList.lookup_insert]
103+
obtain ⟨⟨⟨tn, tc⟩, tr⟩, td⟩ := ht₂
104+
split <;> rename_i h'
105+
· subst h'
106+
simp_all
107+
· simp_all? says simp_all only [ne_eq, hasNestedIf, Bool.or_self, hasConstantIf,
108+
and_self, hasRedundantIf, Bool.or_false, beq_eq_false_iff_ne, not_false_eq_true,
109+
disjoint, List.disjoint, Bool.and_true, Bool.and_eq_true, decide_eq_true_eq',
110+
true_and]
111+
constructor <;> assumption
112+
· have := ht₃ w
113+
have := he₃ w
114+
by_cases w = v
115+
· subst h; simp_all
116+
· simp_all? says simp_all only [Option.elim, ne_eq, normalized, Bool.and_eq_true,
117+
Bool.not_eq_true', not_false_eq_true, AList.lookup_insert_ne]
118+
obtain ⟨⟨⟨en, ec⟩, er⟩, ed⟩ := he₂
119+
split at b <;> rename_i h'
120+
· subst h'; simp_all
121+
· simp_all only [ne_eq, vars, List.singleton_append, List.cons_append,
122+
Bool.not_eq_true, List.mem_cons, List.mem_append, false_or]
123+
cases b <;> simp_all⟩
124+
| some b =>
125+
have ⟨e', he'⟩ := normalize' l (.ite (lit b) t e)
126+
⟨e', by simp_all⟩
127+
termination_by normalize' e => e.normSize'
128+
129+
example : IfNormalization :=
130+
⟨fun e => (normalize' ∅ e).1,
131+
fun e => ⟨(normalize' ∅ e).2.2.1, by simp [(normalize' ∅ e).2.1]⟩⟩

0 commit comments

Comments
 (0)