Zulip Chat Archive
Stream: lean4
Topic: how do i name side variables in induction?
Jared green (Feb 24 2024 at 23:16):
i was trying to prove this (subnormal) but cannot reference unnamed variables. and i dont know how to make it so they are named.
import Init.Data.List
import Std.Data.List
import Mathlib.Data.List.Dedup
import Mathlib.Data.List.Pairwise
import Mathlib.Data.List.Join
import Mathlib.Data.List.Basic
import Mathlib.Data.List.Defs
import Mathlib.Data.List.Infix
import Mathlib.Data.List.Lattice
import Mathlib.Data.List.Lemmas
import Mathlib.Data.Bool.AllAny
import Mathlib.Data.Bool.Basic
open Classical
variable {α : Type}[h : DecidableEq α]
inductive normalizable α (pred : α -> Prop)
where
| atom : α -> (normalizable α pred)
| And : (normalizable α pred) -> (normalizable α pred) -> normalizable α pred
| Or : (normalizable α pred) -> (normalizable α pred) -> normalizable α pred
| Not : normalizable α pred -> normalizable α pred
deriving DecidableEq
namespace normalizable
@[reducible]
def toProp (n : normalizable α pred) : Prop :=
match n with
| atom a => pred a
| And a b => toProp a ∧ toProp b
| Or a b => (toProp a) ∨ toProp b
| Not i => ¬(toProp i)
@[simp]
theorem toProp_not : toProp (Not n₁) ↔ ¬ toProp n₁ := Iff.rfl
@[simp]
theorem toProp_and : toProp (And n₁ n₂) ↔ toProp n₁ ∧ toProp n₂ := Iff.rfl
@[simp]
theorem toProp_or : toProp (Or n₁ n₂) ↔ toProp n₁ ∨ toProp n₂ := Iff.rfl
@[simp]
theorem toProp_atom {a : α} : toProp (atom a : normalizable α pred) ↔ pred a := Iff.rfl
def subnormalize (n : (normalizable α pred)) : List (List (List (normalizable α pred))) :=
match n with
| Or a b => [[a,n],[b,n],[Not a,Not b, Not n]] :: (List.append (subnormalize a) (subnormalize b))
| And a b => [[a,b,n],[Not a,Not n],[Not b,Not n]] :: (List.append (subnormalize a) (subnormalize b))
| Not i => [[n,Not i],[Not n, i]] :: (subnormalize i)
| atom _ => [[[n],[Not n]]]
def normalize : normalizable α pred -> List (List (List (normalizable α pred))) := fun o =>
[[o]] :: (subnormalize o)
def nStrip (n : normalizable α pred) : Bool × normalizable α pred :=
match n with
| Not i => (false,i)
| i => (true,i)
def booleanize (n : List (List (List (normalizable α pred)))) : List (List (List (Bool × normalizable α pred))) :=
n.map (fun x => x.map (fun y => y.map (fun z => nStrip z)))
def normalizel (n : normalizable α pred) : List (List (List (Bool × normalizable α pred))) :=
booleanize (normalize n)
def wToProp (w : Bool × normalizable α pred) : Prop :=
if w.fst then toProp w.snd else ¬(toProp w.snd)
def sToProp (s : List (Bool × normalizable α pred)) : Prop :=
s.all (fun x => wToProp x)
def gToProp (g : List (List (Bool × normalizable α pred))) : Prop :=
g.any (fun x => sToProp x)
def nToProp (n : List (List (List (Bool × normalizable α pred)))) : Prop :=
n.all (fun x => gToProp x)
def fToProp (n : List (List (List (normalizable α pred)))) : Prop :=
n.all (fun x => x.any (fun y => y.all (fun z => toProp z)))
theorem nStrip_equiv : ∀ n : normalizable α pred, toProp n <-> wToProp (nStrip n) :=
by
intro n
unfold nStrip
induction n
simp
unfold wToProp
simp
simp
unfold wToProp
simp
unfold wToProp
simp
simp
unfold wToProp
simp
theorem booleanize_eqiv : ∀ n : List (List (List (normalizable α pred))), fToProp n <-> nToProp (booleanize n) :=
by
intro n
unfold nToProp
simp
unfold fToProp
simp
unfold booleanize
simp
unfold gToProp
simp
unfold sToProp
simp
simp [nStrip_equiv]
theorem andGateTaut : (¬ a ∧ ¬(a ∧ b)) ∨ (¬ b ∧ ¬(a ∧ b)) ∨ (a ∧ b ∧ (a ∧ b)) :=
by
cases Classical.em a
cases Classical.em b
right
right
constructor
assumption
constructor
assumption
constructor
assumption
assumption
right
left
constructor
assumption
push_neg
intro
assumption
left
constructor
assumption
rw [and_comm]
push_neg
intro
assumption
theorem orGateTaut : (a ∧ (a ∨ b)) ∨ (b ∧ (a ∨ b)) ∨ ((¬ a) ∧ (¬b) ∧ ¬(a ∨ b)) = true :=
by
simp
cases Classical.em a
left
constructor
assumption
left
assumption
right
cases Classical.em b
left
constructor
assumption
right
assumption
right
constructor
assumption
constructor
assumption
push_neg
constructor
assumption
assumption
theorem notGateTaut : (a ∧ ¬(¬ a)) ∨ (¬ a ∧ ¬ a) = true :=
by
simp
apply Classical.em
theorem all_and : List.all ( a ++ b) c <-> List.all a c ∧ List.all b c :=
by
simp
constructor
intro ha
constructor
intro b
intro hb
apply ha
left
exact hb
intro c
intro hc
apply ha
right
exact hc
intro ha
intro b
intro hb
cases hb
apply ha.left
assumption
apply ha.right
assumption
theorem subnormal : ∀ n : normalizable α pred, fToProp (subnormalize n) :=
by
intro n
induction n with a b c d e f g h i --name all side variables here
unfold subnormalize
unfold fToProp
simp
unfold toProp
apply Classical.em
unfold subnormalize
simp
unfold fToProp
rw [List.all_cons]
simp only [List.any_cons, List.all_cons, List.all_nil, Bool.and_true, List.any_nil,
Bool.or_false, Bool.and_eq_true, Bool.or_eq_true, decide_eq_true_eq,
List.mem_append, List.any_eq_true]
constructor
rw [toProp_not]
rw [toProp_and]
sorry --should be andGateTaut
rw [all_and]
constructor
assumption
assumption
unfold fToProp
unfold subnormalize
rw [List.all_cons]
simp only [List.any_cons, List.all_cons, toProp_or, List.all_nil, Bool.and_true, toProp_not,
List.any_nil, Bool.or_false, List.append_eq, Bool.and_eq_true, Bool.or_eq_true,
decide_eq_true_eq, List.mem_append, List.any_eq_true]
constructor
rw [toProp_not]
rw [toProp_or]
sorry --should be orGateTaut
rw [all_and]
constructor
assumption
assumption
unfold fToProp
unfold subnormalize
rw [List.all_cons]
simp only [List.any_cons, List.all_cons, toProp_not, List.all_nil, Bool.and_true, Bool.and_self,
not_not, List.any_nil, Bool.or_false, Bool.and_eq_true, Bool.or_eq_true, decide_eq_true_eq,
List.any_eq_true]
constructor
sorry --should be notGateTaut
assumption
Timo Carlin-Burns (Feb 24 2024 at 23:43):
If you want to name your variables all on one line like that, you can use induction'
instead of induction
Jared green (Feb 25 2024 at 01:36):
theorem subnormal : ∀ n : normalizable α pred, fToProp (subnormalize n) :=
by
intro n
induction' n with a b c d e f g i j k l
unfold subnormalize
unfold fToProp
simp
unfold toProp
apply Classical.em
unfold subnormalize
simp
unfold fToProp
rw [List.all_cons]
simp only [List.any_cons, List.all_cons, List.all_nil, Bool.and_true, List.any_nil,
Bool.or_false, Bool.and_eq_true, Bool.or_eq_true, decide_eq_true_eq,
List.mem_append, List.any_eq_true]
constructor
rw [toProp_not]
rw [toProp_and]
exact andGateTaut (toProp b)
rw [all_and]
constructor
assumption
assumption
unfold fToProp
unfold subnormalize
rw [List.all_cons]
simp only [List.any_cons, List.all_cons, toProp_or, List.all_nil, Bool.and_true, toProp_not,
List.any_nil, Bool.or_false, List.append_eq, Bool.and_eq_true, Bool.or_eq_true,
decide_eq_true_eq, List.mem_append, List.any_eq_true]
constructor
rw [toProp_not]
rw [toProp_or]
exact orGateTaut (toProp f)
rw [all_and]
constructor
assumption
assumption
unfold fToProp
unfold subnormalize
rw [List.all_cons]
simp only [List.any_cons, List.all_cons, toProp_not, List.all_nil, Bool.and_true, Bool.and_self,
not_not, List.any_nil, Bool.or_false, Bool.and_eq_true, Bool.or_eq_true, decide_eq_true_eq,
List.any_eq_true]
constructor
exact
unfold fToProp at l --apparently this nor 'assumption' work like it did before.
Ruben Van de Velde (Feb 25 2024 at 07:12):
If you write induction x
in Vs code, you should get a blue lightbulb too click on which can create a skeleton that allows naming the variables
Jared green (Feb 25 2024 at 12:16):
now i have a different problem. shall i start a new discussion for it?
Last updated: May 02 2025 at 03:31 UTC