record & remove boilerplate

GroundZero/Algebra/Group/Subgroup.lean

@@ -38,25 +38,12 @@ namespace Group
 
   hott def isSubgroup.prop (φ : G.subset) : prop (G.isSubgroup φ) :=
   begin
-    apply productProp; apply Ens.prop; apply productProp;
-    -- TODO: fix “repeat” to able handle this case
-    { apply piProp; intro;
-      apply piProp; intro;
-      apply piProp; intro;
-      apply piProp; intro;
-      apply Ens.prop };
-    { apply piProp; intro;
-      apply piProp; intro;
-      apply Ens.prop };
+    apply productProp; apply Ens.prop; apply productProp <;>
+    { repeat first | (apply piProp; intro) | apply Ens.prop }
   end
 
   hott def isNormal.prop (φ : G.subset) : prop (G.isNormal φ) :=
-  begin
-    apply piProp; intro;
-    apply piProp; intro;
-    apply piProp; intro;
-    apply Ens.prop
-  end
+  by repeat first | (apply piProp; intro) | apply Ens.prop
 
   hott def subgroup.ext {φ ψ : G.subgroup} (ρ : φ.set = ψ.set) : φ = ψ :=
   begin fapply Sigma.prod; exact ρ; apply isSubgroup.prop end

GroundZero/Algebra/Transformational.lean

@@ -25,7 +25,7 @@ namespace GroundZero.Algebra
      http://www.math.uchicago.edu/~may/VIGRE/VIGRE2006/PAPERS/Sternberg.pdf
   -/
 
-  structure gis (M : Type u) (G : Group) :=
+  record gis (M : Type u) (G : Group) :=
   (ι     : M → M → G.carrier)
   (trans : Π x y z, G.φ (ι x y) (ι y z) = ι x z)
   (full  : Π g x, contr (Σ y, ι x y = g))
@@ -88,7 +88,7 @@ namespace GroundZero.Algebra
     hott def transInv (x y z : M) : (L.ι x y) * (L.ι z y)⁻¹ = L.ι x z :=
     begin transitivity; apply ap; apply inv; apply L.trans end
 
-    hott def propι : Π g x, prop (Σ y, L.ι x y = g) :=
+    hott corollary propι : Π g x, prop (Σ y, L.ι x y = g) :=
     λ g x, contrImplProp (L.full g x)
 
     hott def fixι : Π g x, Σ y, L.ι x y = g :=
@@ -98,32 +98,31 @@ namespace GroundZero.Algebra
     let q := L.propι (L.ι x y) x ⟨y, Id.refl⟩ ⟨x, L.neut x ⬝ Id.inv p⟩;
     ap Sigma.fst (Id.inv q)
 
-    hott def injιᵣ {x y z : M} : L.ι z x = L.ι z y → x = y :=
+    hott lemma injιᵣ {x y z : M} : L.ι z x = L.ι z y → x = y :=
     begin
       intro p; apply L.zero;
       transitivity; symmetry; apply L.trans x z y;
       transitivity; apply ap; exact Id.inv p;
       transitivity; apply L.trans; apply neut
     end
 
-    hott def injιₗ {x y z : M} : L.ι x z = L.ι y z → x = y :=
+    hott lemma injιₗ {x y z : M} : L.ι x z = L.ι y z → x = y :=
     begin
       intro p; apply L.injιᵣ; apply Group.invInj;
       transitivity; apply inv; symmetry;
       transitivity; apply inv;
       exact Id.inv p
     end
 
-    hott def injεᵣ (x y z : M) (H : hset M) :
-      L.ι z x = L.ι z y ≃ x = y :=
+    hott def injεᵣ (x y z : M) (H : hset M) : (L.ι z x = L.ι z y) ≃ x = y :=
     begin
       apply propEquivLemma; apply G.hset; apply H;
       exact injιᵣ L; intro p; induction p; reflexivity
     end
 
     hott def prod {M₁ : Type u} {M₂ : Type v} {G H : Group} : gis M₁ G → gis M₂ H → gis (M₁ × M₂) (G × H) :=
     begin
-      intros L K; fapply gis.mk;
+      intros L K; refine ⟨?_, ?_, ?_⟩;
       { intros m₁ m₂; fapply Prod.mk;
         exact L.ι m₁.1 m₂.1; exact K.ι m₁.2 m₂.2 };
       { intros x y z; fapply Product.prod;
@@ -159,7 +158,7 @@ namespace GroundZero.Algebra
 
     hott def oct (φ : G.subgroup) := HITs.Quotient (octave L φ)
 
-    hott def normal (φ : G.normal) {a₁ a₂ b₁ b₂ : M}
+    hott theorem normal (φ : G.normal) {a₁ a₂ b₁ b₂ : M}
       (p : L.ι a₁ b₁ ∈ φ.set) (q : L.ι a₂ b₂ ∈ φ.set) : G.φ (L.ι a₁ a₂)⁻¹ (L.ι b₁ b₂) ∈ φ.set :=
     begin
       apply transport (· ∈ φ.set); symmetry;
@@ -423,28 +422,28 @@ namespace GroundZero.Algebra
       variable (N : gis A H) (K : gis B H)
       variable {f : A ≃ B}
 
-      hott def preserving.inv₁ :
+      hott lemma preserving.inv₁ :
         preserving N K f.forward → preserving K N f.left :=
       begin
         intros H a b; transitivity; symmetry; apply H;
         apply bimap <;> apply f.forwardLeft
       end
 
-      hott def preserving.inv₂ :
+      hott lemma preserving.inv₂ :
         preserving N K f.forward → preserving K N f.right :=
       begin
         intros H a b; transitivity; symmetry; apply H;
         apply bimap <;> apply f.forwardRight
       end
 
-      hott def reversing.inv₁ :
+      hott lemma reversing.inv₁ :
         reversing N K f.forward → reversing K N f.left :=
       begin
         intros H a b; transitivity; symmetry; apply H;
         apply bimap <;> apply f.forwardLeft
       end
 
-      hott def reversing.inv₂ :
+      hott lemma reversing.inv₂ :
         reversing N K f.forward → reversing K N f.right :=
       begin
         intros H a b; transitivity; symmetry; apply H;
@@ -456,13 +455,15 @@ namespace GroundZero.Algebra
     λ L, ⟨τ.act L, τ.reg L H⟩
 
     hott def rga.encode : rga M Gᵒᵖ → gis M G :=
-    λ ⟨φ, H⟩, ⟨λ a b, (H a b).1.1, begin
+    λ ⟨φ, H⟩, ⟨λ a b, (H a b).1.1,
+    begin
       intros x y z; apply (regular.elim φ H).2 x;
       transitivity; symmetry; apply φ.2.2;
       transitivity; apply ap; apply (H x y).1.2;
       transitivity; apply (H y z).1.2;
       symmetry; apply (H x z).1.2
-    end, begin
+    end,
+    begin
       intros g x; fapply Sigma.mk;
       { existsi φ.1 g x; apply (regular.elim φ H).2 x;
         apply (H _ _).1.2 };
@@ -472,27 +473,14 @@ namespace GroundZero.Algebra
         { apply G.hset } }
     end⟩
 
-    hott def gis.id : Π (L K : gis M G), L.ι ~ K.ι → L = K :=
+    hott lemma gis.id (L K : gis M G) (H : L.ι ~ K.ι) : L = K :=
     begin
-      intro ⟨φ₁, p₁, q₁⟩ ⟨φ₂, p₂, q₂⟩ p';
-      let p : φ₁ = φ₂ := Theorems.funext p';
-      induction p;
-      let q : p₁ = p₂ := begin
-        -- repeat?
-        apply piProp; intro;
-        apply piProp; intro;
-        apply piProp; intro;
-        apply G.hset
-      end;
-      have r : q₁ = q₂ := begin
-        apply piProp; intro;
-        apply piProp; intro;
-        apply contrIsProp
-      end;
-      induction q; induction r; reflexivity
+      fapply Sigma.prod; apply Theorems.funext H; apply sigProp;
+      { repeat first | (apply piProp; intro) | apply G.hset };
+      { intro; repeat first | (apply piProp; intro) | apply contrIsProp }
     end
 
-    hott def rga.eqv (H : hset M) : rga M Gᵒᵖ ≃ gis M G :=
+    hott theorem rga.eqv (H : hset M) : rga M Gᵒᵖ ≃ gis M G :=
     begin
       existsi rga.encode; apply Prod.mk <;> existsi rga.decode H;
       { intro ⟨φ, p⟩; fapply Sigma.prod;
@@ -515,8 +503,7 @@ namespace GroundZero.Algebra
       apply H; symmetry; apply inv
     end
 
-    hott def reversing.desc (f : M → M) (H : reversing L L f)
-      (m : M) : ρ L m (f m) ~ f :=
+    hott theorem reversing.desc (f : M → M) (H : reversing L L f) (m : M) : ρ L m (f m) ~ f :=
     begin
       intro n; apply @injιᵣ M G L _ _ n;
       transitivity; apply ρ.ι;
@@ -525,7 +512,7 @@ namespace GroundZero.Algebra
       symmetry; apply Group.cancelLeft
     end
 
-    hott def reversing.biinv {f : M → M}
+    hott theorem reversing.biinv {f : M → M}
       (H : reversing L L f) (m : M) : biinv f :=
     transport Equiv.biinv (Theorems.funext (reversing.desc L f H m)) (ρ.biinv L m (f m))
   end gis
@@ -562,7 +549,7 @@ namespace GroundZero.Algebra
     -- Set of tone rows
     def R := Orbits (tr φ)
 
-    def M.dodecaphonic (xs : M A) (r : P A) : Prop :=
+    hott def M.dodecaphonic (xs : M A) (r : P A) : Prop :=
     xs.all (λ x, ⟨x ∈ orbit (tr φ) r, Ens.prop x _⟩)
 
     noncomputable hott def R.dodecaphonic (xs : M A) (r : R φ) : Prop :=

GroundZero/HITs/Merely.lean

@@ -116,7 +116,6 @@ namespace Merely
       { apply pathoverFromTrans; symmetry; transitivity;
         apply ap (_ ⬝ ·); symmetry; apply inclUniqClose;
         symmetry; transitivity; apply ap (· ⬝ _ ⬝ _); apply Id.explodeInv;
-        -- TODO: use “iterate” here
         transitivity; symmetry; apply Id.assoc;
         transitivity; symmetry; apply Id.assoc;
         apply ap ((nthGlue x n)⁻¹ ⬝ ·); apply Id.assoc } };

GroundZero/Meta/Notation.lean

@@ -1,4 +1,9 @@
-import Lean.Parser import Lean.Elab.Command import Lean.PrettyPrinter
+import Lean.Parser import Lean.Parser.Command
+import Lean.Elab.Command import Lean.PrettyPrinter
+import Lean.Elab.DeclUtil
+
+import Lean.Elab.PreDefinition
+
 open Lean.Parser Lean.Parser.Term Lean.Elab.Command
 open Lean.PrettyPrinter.Delaborator
 
@@ -233,4 +238,80 @@ partial def parseSubscript : Lean.Syntax → Lean.MacroM Lean.Term
 | `(subscript| ₍$stx₎)        => parseSubscript stx
 | stx                         => Lean.Macro.throwError "invalid subscript"
 
+namespace Record
+  open Lean
+
+  def expandBinderIdent : Syntax → CommandElabM Name
+  | `(Lean.binderIdent| $i:ident) => return i.getId
+  | stx                           => throwErrorAt stx "expected ident"
+
+  def expandBEBinder : Syntax → TSyntax `term × TSyntaxArray `Lean.binderIdent
+  | `(bracketedExplicitBinders| ($[$xs]* : $t)) => (t, xs)
+  | _                                           => default
+
+  def withImplicits {α : Type} (xs : Array Expr) (k : MetaM α) : MetaM α :=
+  do {
+    let mut lctx ← getLCtx;
+    for x in xs do {
+      if (lctx.get! x.fvarId!).binderInfo.isExplicit then {
+        lctx := lctx.setBinderInfo x.fvarId! BinderInfo.implicit;
+      }
+    }
+    withReader (λ ctx => {ctx with lctx := lctx}) k
+  }
+
+  def declAccessor (tname fname : Name) (t e : Expr) (lparams : List Name) : Elab.Command.CommandElabM Unit :=
+  do {
+    let bvar ← Elab.Term.mkFreshBinderName;
+
+    let lam ← liftTermElabM <|
+      Meta.forallTelescope t λ xs _ =>
+      do mkAppN (mkConst tname (lparams.map Level.param)) xs
+      |> (mkLambda bvar BinderInfo.default · e)
+      |> Meta.mkLambdaFVars xs
+      |> withImplicits xs;
+
+    let typ ← liftTermElabM (Meta.inferType lam);
+    Elab.Command.liftCoreM <| addAndCompile <| Declaration.defnDecl {
+      name        := tname ++ fname,
+      levelParams := lparams,
+      type        := typ,
+      value       := lam,
+      hints       := ReducibilityHints.abbrev,
+      safety      := DefinitionSafety.safe
+    }
+  }
+
+  abbrev sigfst := mkProj ``Sigma 0
+  abbrev sigsnd := mkProj ``Sigma 1
+
+  elab "record " id:declId sig:optDeclSig " :=" ppSpace fields:(ppSpace bracketedExplicitBinders)+ : command =>
+  do {
+    unless (fields.size > 0) do throwErrorAt id "empty record is disallowed";
+
+    let (e, is) := expandBEBinder fields.back;
+
+    let term ← if is.size > 1 then `(Σ $(fields.pop)* ($is.pop* : $e), $e)
+                              else `(Σ $(fields.pop)*, $e);
+    elabCommand (← `(def $id $sig := $term));
+    if (← get).messages.hasErrors then return;
+
+    let ns ← getCurrNamespace;
+    let tname := ns ++ (id.raw.getArg 0).getId;
+
+    let ci ← getConstInfo tname;
+
+    let ids ← fields.concatMapM λ stx =>
+      Array.mapM expandBinderIdent
+        (expandBEBinder stx).2;
+
+    let mut acc := mkBVar 0;
+    for ident in ids.pop do {
+      declAccessor tname ident ci.type (sigfst acc) ci.levelParams;
+      acc := sigsnd acc;
+    }
+    declAccessor tname ids.back ci.type acc ci.levelParams
+  }
+end Record
+
 end GroundZero.Meta.Notation

GroundZero/Structures.lean

@@ -208,23 +208,16 @@ section
     apply propIsSet (contrImplProp ⟨x, u⟩)
   end
 
-  -- TODO: apply “repeat” tactic
   hott def propIsProp {A : Type u} : prop (prop A) :=
   begin
-    intros f g;
-    apply HITs.Interval.funext; intro;
-    apply HITs.Interval.funext; intro;
-    apply propIsSet; assumption
+    intros f g; repeat first | (apply HITs.Interval.funext; intro)
+                             | (apply propIsSet; assumption)
   end
 
   hott def setIsProp {A : Type u} : prop (hset A) :=
   begin
-    intros f g;
-    apply HITs.Interval.funext; intro;
-    apply HITs.Interval.funext; intro;
-    apply HITs.Interval.funext; intro;
-    apply HITs.Interval.funext; intro;
-    apply setImplGroupoid; assumption
+    intros f g; repeat first | (apply HITs.Interval.funext; intro)
+                             | (apply setImplGroupoid; assumption)
   end
 
   hott def ntypeIsProp : Π (n : hlevel) {A : Type u}, prop (is-n-type A)
@@ -771,25 +764,13 @@ end
 
 hott def eqrel (A : Type u) := Σ φ, @iseqrel A φ
 
--- TODO: repeat
 hott def iseqrel.prop {A : Type u} {R : hrel A} : prop (iseqrel R) :=
 begin
   apply Structures.productProp;
-  { intros f g; apply Theorems.funext;
-    intro x; apply (R x x).2 };
-  apply Structures.productProp;
-  { intros f g;
-    apply Theorems.funext; intro;
-    apply Theorems.funext; intro;
-    apply Theorems.funext; intro;
-    apply (R _ _).2 };
-  { intros f g;
-    apply Theorems.funext; intro;
-    apply Theorems.funext; intro;
-    apply Theorems.funext; intro;
-    apply Theorems.funext; intro;
-    apply Theorems.funext; intro;
-    apply (R _ _).2 }
+  { intros f g; apply Theorems.funext; intro x; apply (R x x).2 };
+  apply Structures.productProp <;>
+  { intros f g; repeat first | (apply Theorems.funext; intro)
+                             | apply (R _ _).2 }
 end
 
 section

GroundZero/Theorems/Univalence.lean

@@ -208,7 +208,6 @@ begin
     | Sum.inr p₂, Sum.inl q₁ => _
     | Sum.inl p₁, Sum.inr q₂ => _
     | Sum.inr p₂, Sum.inr q₂ => _;
-    -- TODO: apply “or” here somehow
     { apply Proto.Empty.elim; apply ffNeqTt;
       apply eqvInj ⟨φ, H⟩; exact p₁ ⬝ q₁⁻¹ };
     { transitivity; apply ap (bool.encode · x); apply p₂;