update lean to 4.11rc2

.github/workflows/check_proofs.yml

@@ -22,7 +22,7 @@ jobs:
         run: |
           curl -O --location https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh
           chmod u+x elan-init.sh
-          ./elan-init.sh -y --default-toolchain leanprover/lean4:v4.2.0-rc4
+          ./elan-init.sh -y --default-toolchain leanprover/lean4:v4.11.0-rc2
           echo "Adding location $HOME/.elan/bin to PATH..."
           echo "$HOME/.elan/bin" >> $GITHUB_PATH
 

Katydid/Conal/Calculus.lean

@@ -66,7 +66,7 @@ attribute [simp] ν' δ'
 
 -- ν∅  : ν ∅ ≡ ⊥
 -- ν∅ = refl
-theorem nullable_emptySet:
+def nullable_emptySet:
   ∀ (α: Type),
     @ν' α ∅ ≡ PEmpty := by
   intro α
@@ -75,7 +75,7 @@ theorem nullable_emptySet:
 
 -- ν𝒰  : ν 𝒰 ≡ ⊤
 -- ν𝒰 = refl
-theorem nullable_universal:
+def nullable_universal:
   ∀ (α: Type),
     @ν' α 𝒰 ≡ PUnit := by
   intro α
@@ -88,7 +88,7 @@ theorem nullable_universal:
 --   (λ { tt → refl })
 --   (λ { tt → refl })
 --   (λ { refl → refl })
-theorem nullable_emptyStr:
+def nullable_emptyStr:
   ∀ (α: Type),
     @ν' α ε ≃ PUnit := by
   intro α
@@ -104,7 +104,7 @@ theorem nullable_emptyStr:
   intro _
   simp
 
-theorem nullable_emptyStr':
+def nullable_emptyStr':
   ∀ (α: Type),
     @ν' α ε ≃ PUnit :=
     fun _ => Equiv.mk
@@ -115,7 +115,7 @@ theorem nullable_emptyStr':
 
 -- ν`  : ν (` c) ↔ ⊥
 -- ν` = mk↔′ (λ ()) (λ ()) (λ ()) (λ ())
-theorem nullable_char:
+def nullable_char:
   ∀ (c: α),
     ν' (char c) ≃ PEmpty := by
   intro α
@@ -130,7 +130,7 @@ theorem nullable_char:
   sorry
   sorry
 
-theorem nullable_char':
+def nullable_char':
   ∀ (c: α),
     ν' (char c) -> PEmpty := by
   intro
@@ -145,7 +145,7 @@ theorem nullable_char':
 
 -- ν∪  : ν (P ∪ Q) ≡ (ν P ⊎ ν Q)
 -- ν∪ = refl
-theorem nullable_or:
+def nullable_or:
   ∀ (P Q: dLang α),
     ν' (P ⋃ Q) ≡ (Sum (ν' P) (ν' Q)) := by
   intro P Q
@@ -154,7 +154,7 @@ theorem nullable_or:
 
 -- ν∩  : ν (P ∩ Q) ≡ (ν P × ν Q)
 -- ν∩ = refl
-theorem nullable_and:
+def nullable_and:
   ∀ (P Q: dLang α),
     ν' (P ⋂ Q) ≡ (Prod (ν' P) (ν' Q)) := by
   intro P Q
@@ -163,7 +163,7 @@ theorem nullable_and:
 
 -- ν·  : ν (s · P) ≡ (s × ν P)
 -- ν· = refl
-theorem nullable_scalar:
+def nullable_scalar:
   ∀ (s: Type) (P: dLang α),
     ν' (dLang.scalar s P) ≡ (Prod s (ν' P)) := by
   intro P Q
@@ -176,7 +176,7 @@ theorem nullable_scalar:
 --   (λ { (νP , νQ) → ([] , []) , refl , νP , νQ })
 --   (λ { (νP , νQ) → refl } )
 --   (λ { (([] , []) , refl , νP , νQ) → refl})
-theorem nullable_concat:
+def nullable_concat:
   ∀ (P Q: dLang α),
     ν' (P, Q) ≃ (Prod (ν' Q) (ν' P)) := by
   -- TODO
@@ -210,15 +210,15 @@ theorem nullable_concat:
 --   ≈⟨ ν✪ ⟩
 --     (ν P) ✶
 --   ∎ where open ↔R
-theorem nullable_star:
+def nullable_star:
   ∀ (P: dLang α),
     ν' (P *) ≃ List (ν' P) := by
   -- TODO
   sorry
 
 -- δ∅  : δ ∅ a ≡ ∅
 -- δ∅ = refl
-theorem derivative_emptySet:
+def derivative_emptySet:
   ∀ (a: α),
     (δ' ∅ a) ≡ ∅ := by
   intro a
@@ -227,7 +227,7 @@ theorem derivative_emptySet:
 
 -- δ𝒰  : δ 𝒰 a ≡ 𝒰
 -- δ𝒰 = refl
-theorem derivative_universal:
+def derivative_universal:
   ∀ (a: α),
     (δ' 𝒰 a) ≡ 𝒰 := by
   intro a
@@ -237,7 +237,7 @@ theorem derivative_universal:
 -- δ𝟏  : δ 𝟏 a ⟷ ∅
 -- δ𝟏 = mk↔′ (λ ()) (λ ()) (λ ()) (λ ())
 -- TODO: Redo this definition to do extensional isomorphism: `⟷` properly
-theorem derivative_emptyStr:
+def derivative_emptyStr:
   ∀ (a: α),
     (δ' ε a) ≡ ∅ := by
   -- TODO
@@ -250,7 +250,7 @@ theorem derivative_emptyStr:
 --   (λ { (refl , refl) → refl })
 --   (λ { refl → refl })
 -- TODO: Redo this definition to do extensional isomorphism: `⟷` properly
-theorem derivative_char:
+def derivative_char:
   ∀ (a: α) (c: α),
     (δ' (char c) a) ≡ dLang.scalar (a ≡ c) ε := by
     intros a c
@@ -262,7 +262,7 @@ theorem derivative_char:
 
 -- δ∪  : δ (P ∪ Q) a ≡ δ P a ∪ δ Q a
 -- δ∪ = refl
-theorem derivative_or:
+def derivative_or:
   ∀ (a: α) (P Q: dLang α),
     (δ' (P ⋃ Q) a) ≡ ((δ' P a) ⋃ (δ' Q a)) := by
   intro a P Q
@@ -271,7 +271,7 @@ theorem derivative_or:
 
 -- δ∩  : δ (P ∩ Q) a ≡ δ P a ∩ δ Q a
 -- δ∩ = refl
-theorem derivative_and:
+def derivative_and:
   ∀ (a: α) (P Q: dLang α),
     (δ' (P ⋂ Q) a) ≡ ((δ' P a) ⋂ (δ' Q a)) := by
   intro a P Q
@@ -280,7 +280,7 @@ theorem derivative_and:
 
 -- δ·  : δ (s · P) a ≡ s · δ P a
 -- δ· = refl
-theorem derivative_scalar:
+def derivative_scalar:
   ∀ (a: α) (s: Type) (P: dLang α),
     (δ (dLang.scalar s P) a) ≡ (dLang.scalar s (δ' P a)) := by
   intro a s P
@@ -298,7 +298,7 @@ theorem derivative_scalar:
 --   (λ { (([] , .(a ∷ w)) , refl , νP , Qaw) → refl
 --      ; ((.a ∷ u , v) , refl , Pu , Qv) → refl })
 -- TODO: Redo this definition to do extensional isomorphism: `⟷` properly
-theorem derivative_concat:
+def derivative_concat:
   ∀ (a: α) (P Q: dLang α),
   -- TODO: Redo this definition to do extensional isomorphism: `⟷` properly
     (δ' (P , Q) a) ≡ dLang.scalar (ν' P) ((δ' Q a) ⋃ ((δ' P a), Q)) := by
@@ -338,7 +338,7 @@ theorem derivative_concat:
 --     ((ν P) ✶ · (δ P a ⋆ P ☆)) w
 --   ∎ where open ↔R
 -- TODO: Redo this definition to do extensional isomorphism: `⟷` properly
-theorem derivative_star:
+def derivative_star:
   ∀ (a: α) (P: dLang α),
   -- TODO: Redo this definition to do extensional isomorphism: `⟷` properly
     (δ' (P *) a) ≡ dLang.scalar (List (ν' P)) (δ' P a, P *) := by

Katydid/Conal/Language.lean

@@ -163,10 +163,10 @@ inductive Lang : (List α -> Type u) -> Type (u + 1) where
 
 #check @Lang.casesOn
 
--- 𝜈 : Lang P → Dec (⋄.𝜈 P)
-theorem ν {α: Type u} {P: dLang α} (f: Lang P): Dec (dLang.ν P) := by
-  induction f with
-  | universal => exact unit?
+-- TODO: 𝜈 : Lang P → Dec (⋄.𝜈 P)
+-- theorem ν {α: Type u} {P: dLang α} (f: Lang P): Dec (dLang.ν P) := by
+--   induction f with
+--   | universal => exact unit?
 
 -- TODO: rewrite ν using casesOn
 -- def ν' {α: Type u} {P: dLang α} (f: Lang P): Dec (dLang.ν P) := by

Katydid/Std/Balistic.lean

@@ -276,6 +276,7 @@ example (xs ys zs: List α):
   ys = zs -> ys ++ xs = zs ++ xs := by
   list_app
 
+-- set_option linter.constructorNameAsVariable false in
 local elab "wreck_exists" : tactic => newTactic do
   let hyps ← getHypotheses
   for (name, ty) in hyps do

Katydid/Std/Lists.lean

@@ -488,7 +488,7 @@ theorem list_take_take (n n: Nat) (xs: List α):
       unfold minOfLe
       simp only
       split
-      case succ.succ.inl h =>
+      next h =>
         rw [nat_succ_le_succ_iff] at h
         cases xs with
         | nil =>
@@ -506,7 +506,7 @@ theorem list_take_take (n n: Nat) (xs: List α):
           have ihn' : _ := @ihn m xs
           rw [hmin] at ihn'
           exact ihn'
-      case succ.succ.inr h =>
+      next h =>
         rw [nat_succ_le_succ_iff] at h
         cases xs with
         | nil =>
@@ -687,14 +687,13 @@ theorem list_take_length (n: Nat) (xs: List α):
   unfold minOfLe
   simp only [length_take, ge_iff_le]
   split
-  case inl =>
+  next =>
     rename_i c
     unfold min; unfold instMinNat; unfold minOfLe; simp only [ite_eq_left_iff, not_le]
     intro c'
     linarith
-  case inr =>
+  next =>
     rename_i c
-    have c' := gt_of_not_le c
     unfold min; unfold instMinNat; unfold minOfLe; simp only [ite_eq_right_iff]
     intro c''
     linarith

Katydid/Std/Ltac.lean

@@ -1,4 +1,4 @@
-import Std.Lean.Meta.UnusedNames
+import Lean.Meta.Tactic.Util
 import Qq
 open Qq
 
@@ -108,8 +108,9 @@ example (H: x): x /\ x := by
   example_assumption_tactic
 
 -- Creates a fresh variable with the suggested name.
-def fresh [Monad m] [Lean.MonadLCtx m] (suggestion : Lean.Name) : m Lean.Syntax.Ident := do
-  let name ← Lean.Meta.getUnusedUserName suggestion
+def fresh [Monad m] [Lean.MonadLCtx m] (suggestion : String) : m Lean.Syntax.Ident := do
+  let lctx ← Lean.MonadLCtx.getLCtx
+  let name := lctx.getUnusedName (Lean.Name.mkSimple suggestion)
   return Lean.mkIdent name
 
 -- Removes quotes from the start of a string
@@ -186,19 +187,3 @@ example (P: (A -> B) /\ A): B := by
 --  - https://github.com/leanprover-community/mathlib4/blob/2d97a156aa63b50456ed3e5a7d6af3096ac7958e/Mathlib/Tactic/Tauto.lean
 --  - https://github.com/leanprover-community/mathlib4/blob/bac7310cc18d6ed292606d26ccb5fb9ffc697c7a/Mathlib/Tactic/Slice.lean
 --  - https://github.com/siddhartha-gadgil/LeanAide
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-

Katydid/Std/Tipe2.lean

@@ -25,7 +25,7 @@ example : 1 ≡ 1 := by
 -- TODO: How can we make rewrite easier, without needing to destruct first?
 --   TODO: if all else fails, write a tactic
 
-theorem rewrite_test:
+def rewrite_test:
   ∀ (_: a ≡ b) (_: b ≡ c),
     a ≡ c := by
   intro ab bc
@@ -37,7 +37,7 @@ theorem rewrite_test:
     | mk bc =>
       rw [bc]
 
-theorem rewrite_test':
+def rewrite_test':
   ∀ (_: a ≡ b) (_: b ≡ c),
     a ≡ c := by
   intro ab bc
@@ -55,7 +55,7 @@ def rewrite_test'' (ab: a ≡ b) (bc: b ≡ c): a ≡ c :=
   match (ab, bc) with
   | ⟨ ⟨ ab' ⟩ , ⟨ bc' ⟩ ⟩ => by sorry
 
-theorem rewrite_test''':
+def rewrite_test''':
   ∀ (_: a ≡ b) (_: b ≡ c),
     a ≡ c := by
   intro ab bc