abbreviations & style changes & lakefile.lean

GroundZero/Meta/HottTheory.lean

@@ -96,39 +96,50 @@ partial def checkDeclAux (chain : List Name) (tag : Syntax) (name : Name) : Meta
   let env ← getEnv
 
   if ¬(← checked? name) then
-    checkNotNotHoTT tag env name
+    checkNotNotHoTT tag env name;
     match env.find? name with
     | some (ConstantInfo.recInfo v) =>
       List.forM v.all (checkLargeElim tag chain)
     | some (ConstantInfo.opaqueInfo v) =>
       throwErrorAt tag "uses unsafe opaque: {renderChain chain}"
     | some info =>
       match info.value? with
+      | none      => return ()
       | some expr => Array.forM (λ n => checkDeclAux (n :: chain) tag n)
                                 expr.getUsedConstants
-      | none => return ()
     | none => throwError "unknown identifier “{name}”"
   else return ()
 
 def checkDecl := checkDeclAux []
 
-def declTok : Parser.Parser :=
+def defTok := leading_parser
     "def "         <|> "definition " <|> "theorem "   <|> "lemma "
 <|> "proposition " <|> "corollary "  <|> "principle " <|> "claim "
 <|> "statement "   <|> "paradox "    <|> "remark "    <|> "exercise "
 
-def declDef := leading_parser
-  Parser.ppIndent optDeclSig >> declVal >> optDefDeriving >> terminationSuffix
+/--
+  `reducible` and `inline` attributes are automatically added to abbreviations.
+-/
+def abbrevTok := leading_parser "abbrev " <|> "abbreviation "
+
+def exampleTok := leading_parser "example " <|> "counterexample "
 
-def decl        := leading_parser declTok >> declId >> declDef
-def declExample := leading_parser ("example " <|> "counterexample ") >> declDef
+def declDef     := leading_parser Parser.ppIndent optDeclSig >> declVal >> optDefDeriving >> terminationSuffix
+def decl        := leading_parser (defTok <|> abbrevTok) >> declId >> declDef
+def declExample := leading_parser exampleTok >> declDef
+
+/--
+  Adds declaration and throws an error whenever it uses singleton elimination and/or
+  any other principle (i.e. global choice) inconsistent with HoTT.
+-/
+def hottPrefix := leading_parser "hott "
 
 @[command_parser] def hott :=
-leading_parser declModifiers false >> "hott " >> (decl <|> declExample)
+leading_parser declModifiers false >> hottPrefix >> (decl <|> declExample)
 
-open Elab.Command
+open Elab Elab.Command
 
-def defAndCheck (tag declMods declId declDef : Syntax) : CommandElabM Unit := do {
+def defAndCheck (tag declMods declId declDef : Syntax) : CommandElabM Name := do {
   let ns ← getCurrNamespace;
   let declName := ns ++ declId[0].getId;
 
@@ -141,22 +152,28 @@ def defAndCheck (tag declMods declId declDef : Syntax) : CommandElabM Unit := do
     liftTermElabM (checkDecl tag declName);
     modifyEnv (λ env => hottDecls.addEntry env declName)
   }
+
+  return declName
 }
 
+def abbrevAttrs : Array Attribute :=
+#[{name := `inline}, {name := `reducible}]
+
 @[command_elab «hott»] def elabHoTT : CommandElab :=
 λ stx => do {
-  let #[mods, _, cmd] := stx.getArgs | throwError "invalid declaration";
+  let #[mods, _, cmd] := stx.getArgs | throwError "incomplete declaration";
 
   match cmd.getArgs with
-  | #[_, declId, declDef] => defAndCheck declId mods declId declDef
-  | #[tok, declDef]       => do {
+  | #[tok, declId, declDef] => do {
+    let declName ← defAndCheck declId mods declId declDef;
+    if tok.isOfKind ``abbrevTok then liftTermElabM (Term.applyAttributes declName abbrevAttrs)
+  }
+  | #[tok, declDef] =>
     withoutModifyingEnv do {
-      #[mkIdentFrom tok `_example, mkNullNode]
-      |> mkNode ``Parser.Command.declId
-      |> (defAndCheck tok mods · declDef)
+      let declId := mkNode ``declId #[mkIdentFrom tok `_example, mkNullNode];
+      discard (defAndCheck tok mods declId declDef)
     }
-  }
-  | _ => throwError "invalid definition"
+  | _ => throwError "invalid declaration"
 }
 
 end GroundZero.Meta.HottTheory

GroundZero/Proto.lean

@@ -3,28 +3,27 @@ import GroundZero.Meta.Basic
 namespace GroundZero.Proto
 universe u v w
 
-hott def idfun {A : Sort u} : A → A :=
+hott definition idfun {A : Sort u} : A → A :=
 λ a, a
 
 inductive Empty : Type u
 
 attribute [eliminator] Empty.casesOn
 
-def Iff (A : Type u) (B : Type v) :=
-(A → B) × (B → A)
+hott definition Iff (A : Type u) (B : Type v) := (A → B) × (B → A)
 
 infix:30 (priority := high) " ↔ " => Iff
 
-hott def Iff.left  {A : Type u} {B : Type v} (w : A ↔ B) : A → B := w.1
-hott def Iff.right {A : Type u} {B : Type v} (w : A ↔ B) : B → A := w.2
+hott definition Iff.left  {A : Type u} {B : Type v} (w : A ↔ B) : A → B := w.1
+hott definition Iff.right {A : Type u} {B : Type v} (w : A ↔ B) : B → A := w.2
 
-hott def Iff.refl {A : Type u} : A ↔ A :=
+hott definition Iff.refl {A : Type u} : A ↔ A :=
 ⟨idfun, idfun⟩
 
-hott def Iff.symm {A : Type u} {B : Type v} : (A ↔ B) → (B ↔ A) :=
+hott definition Iff.symm {A : Type u} {B : Type v} : (A ↔ B) → (B ↔ A) :=
 λ p, ⟨p.right, p.left⟩
 
-hott def Iff.comp {A : Type u} {B : Type v} {C : Type w} :
+hott definition Iff.comp {A : Type u} {B : Type v} {C : Type w} :
   (A ↔ B) → (B ↔ C) → (A ↔ C) :=
 λ p q, ⟨q.left ∘ p.left, p.right ∘ q.right⟩
 
@@ -36,28 +35,28 @@ notation "𝟎" => Empty
 notation "𝟐" => Bool
 notation "ℕ" => Nat
 
-def Empty.elim {A : Sort u} (xs : Empty) : A :=
+hott definition Empty.elim {A : Sort u} (xs : Empty) : A :=
 nomatch xs
 
-def Bool.elim {A : Sort u} : A → A → 𝟐 → A :=
+hott definition Bool.elim {A : Sort u} : A → A → 𝟐 → A :=
 λ b₁ b₂ b, @Bool.casesOn (λ _, A) b b₁ b₂
 
-def Bottom := Empty.{0}
+hott abbreviation Bottom := Empty.{0}
 notation (priority := low) "⊥" => Bottom
 
 inductive Identity (A : Type u)
 | elem : A → Identity A
 
 attribute [eliminator] Identity.casesOn
 
-def Identity.elim {A : Type u} : Identity A → A
+hott definition Identity.elim {A : Type u} : Identity A → A
 | Identity.elem a => a
 
-def Identity.lift {A : Type u} {B : Type v}
+hott definition Identity.lift {A : Type u} {B : Type v}
   (f : A → B) : Identity A → Identity B
 | Identity.elem a => Identity.elem (f a)
 
-def Identity.lift₂ {A : Type u} {B : Type v} {C : Type w}
+hott definition Identity.lift₂ {A : Type u} {B : Type v} {C : Type w}
   (f : A → B → C) : Identity A → Identity B → Identity C
 | Identity.elem a, Identity.elem b => Identity.elem (f a b)