Lean Notes

2.3. Using cbv with stdlib data structures🔗

cbv also reduces operations on standard-library data structures. A HashSet membership query is not definitionally true:

example : (({} : HashSet Nat).insert 4 |>.contains 4) = true := ⊢ (∅.insert 4).contains 4 = true Tactic `rfl` failed: The left-hand side (∅.insert 4).contains 4 is not definitionally equal to the right-hand side true ⊢ (∅.insert 4).contains 4 = true⊢ (∅.insert 4).contains 4 = true 
Tactic `rfl` failed: The left-hand side
  (∅.insert 4).contains 4
is not definitionally equal to the right-hand side
  true

⊢ (∅.insert 4).contains 4 = true

but cbv evaluates it:

-- set_option trace.Meta.Tactic.cbv true in -- set_option trace.Meta.Tactic.cbv.simprocs true in -- set_option trace.Meta.Tactic.cbv.rewrite true in -- set_option trace.Meta.Tactic.cbv.unfold true in theorem hashset_simp_eval : (({} : HashSet Nat).insert 4 |>.contains 4) = true := ⊢ (∅.insert 4).contains 4 = true All goals completed! 🐙

The generated proof uses the relevant HashSet lemmas:

theorem Probe.hashset_simp_eval : (∅.insert 4).contains 4 = true := of_eq_true (Eq.trans (congrFun' (congrArg Eq (Eq.trans (Eq.trans (congrFun' (congrArg HashSet.contains (congrFun' (congrArg HashSet.insert (Eq.trans (EmptyCollection.emptyCollection.eq_1 (HashSet Nat)) (Eq.trans (congrArg (fun x ↦ x.1) HashSet.instEmptyCollection.eq_1) (Eq.refl HashSet.emptyWithCapacity)))) 4)) 4) HashSet.contains_insert) (Eq.trans (congr (congrArg or (eagerReduce (Eq.refl true))) HashSet.contains_emptyWithCapacity) (Bool.or.eq_1 false)))) true) (eq_self true))#print hashset_simp_eval 
theorem Probe.hashset_simp_eval : (∅.insert 4).contains 4 = true :=
of_eq_true
  (Eq.trans
    (congrFun'
      (congrArg Eq
        (Eq.trans
          (Eq.trans
            (congrFun'
              (congrArg HashSet.contains
                (congrFun'
                  (congrArg HashSet.insert
                    (Eq.trans (EmptyCollection.emptyCollection.eq_1 (HashSet Nat))
                      (Eq.trans (congrArg (fun x ↦ x.1) HashSet.instEmptyCollection.eq_1)
                        (Eq.refl HashSet.emptyWithCapacity))))
                  4))
              4)
            HashSet.contains_insert)
          (Eq.trans (congr (congrArg or (eagerReduce (Eq.refl true))) HashSet.contains_emptyWithCapacity)
            (Bool.or.eq_1 false))))
      true)
    (eq_self true))