S03_Inductive_Structures.lean`

GitHub source file

30 declarations, 9 contain sorry, 0 declared as axioms

Imports (1)

Mathlib.Tactic

Imported by 1 file

MIL.lean

inductive MyListSpace.List line 5 source
no axioms what this means
def MyListSpace2.append line 13 source
no axioms what this means
Statement uses: List
2 instances, coercions and auxiliary constants left out.
def MyListSpace2.map line 17 source
no axioms what this means
Statement uses: List
2 instances, coercions and auxiliary constants left out.
theorem MyListSpace2.nil_append line 24 source
no axioms what this means
Statement uses: List, Eq, MyListSpace2.append, List.nil
Proof uses: rfl
theorem MyListSpace2.cons_append line 26 source
no axioms what this means
Statement uses: List, Eq, MyListSpace2.append, List.cons
Proof uses: rfl
theorem MyListSpace2.map_nil line 29 source
no axioms what this means
Statement uses: Eq, List, MyListSpace2.map, List.nil
Proof uses: rfl
theorem MyListSpace2.map_cons line 31 source
no axioms what this means
Statement uses: List, Eq, MyListSpace2.map, List.cons
Proof uses: rfl
theorem MyListSpace3.append_nil line 44 source
no axioms what this means
Statement uses: List, Eq, HAppend.hAppend, List.nil
6 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MyListSpace3.map_map line 48 source
no axioms what this means
Statement uses: List, Eq, List.map, Function.comp
2 instances, coercions and auxiliary constants left out.
Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem MyListSpace3.append_nil' line 53 source
no axioms what this means
Statement uses: List, Eq, HAppend.hAppend, List.nil
Proof uses: List.rec, Eq.refl, Eq.mpr, List.cons, id, congrArg, List.cons_append
4 instances, coercions and auxiliary constants left out.
Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
theorem MyListSpace3.map_map' line 58 source
standard axioms: propext what this means
Statement uses: List, Eq, List.map, Function.comp
Proof uses: List.rec, Eq.refl, List.nil, of_eq_true, List.cons, Eq.trans, True, congrFun', congrArg, eq_self
Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
def MyListSpace3.reverse sorry line 64 source
depends on sorry what this means
Statement uses: List
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
1 instances, coercions and auxiliary constants left out.
Distinct definitions of this name: MIL/C06_Discrete_Mathematics/solutions/Solutions_S03_Inductive_Structures.lean:11 (different declaration text). Qualify references as MyListSpace3.reverse@path.
theorem MyListSpace3.reverse_append sorry line 66 source
depends on sorry what this means
Statement uses: List, Eq, MyListSpace3.reverse, HAppend.hAppend
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
5 instances, coercions and auxiliary constants left out.
Distinct definitions of this name: MIL/C06_Discrete_Mathematics/solutions/Solutions_S03_Inductive_Structures.lean:15 (same statement text; different proof or body). Qualify references as MyListSpace3.reverse_append@path.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MyListSpace3.reverse_reverse sorry line 69 source
depends on sorry what this means
Statement uses: List, Eq, MyListSpace3.reverse
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
1 instances, coercions and auxiliary constants left out.
Distinct definitions of this name: MIL/C06_Discrete_Mathematics/solutions/Solutions_S03_Inductive_Structures.lean:20 (same statement text; different proof or body). Qualify references as MyListSpace3.reverse_reverse@path.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
inductive BinTree line 73 source
no axioms what this means
Also declared: MIL/C06_Discrete_Mathematics/solutions/Solutions_S03_Inductive_Structures.lean:27 (same declaration text).
def BinTree.size line 79 source
no axioms what this means
Statement uses: BinTree, Nat
2 instances, coercions and auxiliary constants left out.
Also declared: MIL/C06_Discrete_Mathematics/solutions/Solutions_S03_Inductive_Structures.lean:33 (same declaration text).
def BinTree.depth line 83 source
no axioms what this means
Statement uses: BinTree, Nat
2 instances, coercions and auxiliary constants left out.
Also declared: MIL/C06_Discrete_Mathematics/solutions/Solutions_S03_Inductive_Structures.lean:37 (same declaration text).
theorem BinTree.size_le line 87 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: BinTree, LE.le, Nat, BinTree.size, HSub.hSub, HPow.hPow, OfNat.ofNat, BinTree.depth
16 instances, coercions and auxiliary constants left out.
Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
theorem BinTree.depth_le_size sorry line 100 source
depends on sorry what this means
Statement uses: BinTree, LE.le, Nat, BinTree.depth, BinTree.size
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
3 instances, coercions and auxiliary constants left out.
Distinct definitions of this name: MIL/C06_Discrete_Mathematics/solutions/Solutions_S03_Inductive_Structures.lean:41 (different declaration text). Qualify references as BinTree.depth_le_size@path.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def BinTree.flip sorry line 102 source
depends on sorry what this means
Statement uses: BinTree
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
1 instances, coercions and auxiliary constants left out.
Distinct definitions of this name: MIL/C06_Discrete_Mathematics/solutions/Solutions_S03_Inductive_Structures.lean:51 (different declaration text). Qualify references as BinTree.flip@path.
example BinTree.(example at line 104) sorry line 104 source
theorem BinTree.size_flip sorry line 107 source
depends on sorry what this means
Statement uses: BinTree, Eq, Nat, BinTree.size, BinTree.flip
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
1 instances, coercions and auxiliary constants left out.
Distinct definitions of this name: MIL/C06_Discrete_Mathematics/solutions/Solutions_S03_Inductive_Structures.lean:58 (different declaration text). Qualify references as BinTree.size_flip@path.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
inductive PropForm line 110 source
no axioms what this means
Also declared: MIL/C06_Discrete_Mathematics/solutions/Solutions_S03_Inductive_Structures.lean:66 (same declaration text).
def PropForm.eval line 118 source
no axioms what this means
Statement uses: PropForm, Nat, Bool
2 instances, coercions and auxiliary constants left out.
Also declared: MIL/C06_Discrete_Mathematics/solutions/Solutions_S03_Inductive_Structures.lean:74 (same declaration text).
def PropForm.vars line 125 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PropForm, Finset, Nat
2 instances, coercions and auxiliary constants left out.
Also declared: MIL/C06_Discrete_Mathematics/solutions/Solutions_S03_Inductive_Structures.lean:81 (same declaration text).
theorem PropForm.eval_eq_eval line 132 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PropForm, Nat, Bool, Membership.mem, Finset, PropForm.vars, Eq, PropForm.eval
6 instances, coercions and auxiliary constants left out.
Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
theorem PropForm.eval_eq_eval' line 143 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PropForm, Nat, Bool, Membership.mem, Finset, PropForm.vars, Eq, PropForm.eval
6 instances, coercions and auxiliary constants left out.
Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def PropForm.subst line 147 source
no axioms what this means
Statement uses: PropForm, Nat
2 instances, coercions and auxiliary constants left out.
Also declared: MIL/C06_Discrete_Mathematics/solutions/Solutions_S03_Inductive_Structures.lean:88 (same declaration text).
theorem PropForm.subst_eq_of_not_mem_vars sorry line 154 source
depends on sorry what this means
Statement uses: PropForm, Nat, Not, Membership.mem, Finset, PropForm.vars, Eq, PropForm.subst
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
5 instances, coercions and auxiliary constants left out.
Distinct definitions of this name: MIL/C06_Discrete_Mathematics/solutions/Solutions_S03_Inductive_Structures.lean:95 (different declaration text). Qualify references as PropForm.subst_eq_of_not_mem_vars@path.
theorem PropForm.subst_eval_eq sorry line 157 source
depends on sorry what this means
Statement uses: PropForm, Nat, Bool, Eq, PropForm.eval, PropForm.subst, ite
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
3 instances, coercions and auxiliary constants left out.
Distinct definitions of this name: MIL/C06_Discrete_Mathematics/solutions/Solutions_S03_Inductive_Structures.lean:111 (different declaration text). Qualify references as PropForm.subst_eval_eq@path.