Rectification Campaign II: Restrictions, etc. (#230)

* not sure if needed

* fix another potentially subtle bug

* first pass at deleting box modality

* add files that I forgot to check in (Kind.mli, Lvl.mli)

* remove locks, tick constant, etc.

* delete bad idea, push_restriction

* adding explicit support for definitions, don't use "singleton types" for this

* dead code

* fancy typechecking algorithm with judgmental restriction

* start keeping track of which of Evan's brutal examples work

* add evan's brutal stuff to the makefile :)

* do not try to support subtyping between a restriction type & non-restriction type

* Revert "do not try to support subtyping between a restriction type & non-restriction type"

This reverts commit f4df7db.

* start adding more info to tactic input (just adding record for now)

* minor code cleanup

* code simplification

* potential switcharoo ???

* trying to get less owned by things being backwards ??

* pretty printing for debugging

* more partial fixing of resolution bugs

* more debuggable clause lookup

* debugging

* turn off unused-variable error (MAKES DEBUGGING IMPOSSIBLE)

* some reasonable changes

* temporary stop checking boundaries of elim clauses until I rectify

* think I may have fixed typechecking of elim

* minor fix

* first attempt to refine elim clause boundaries again

* tentative fix to evan's other example

* remove comment

* fix another bug found by @ecavallo (keep 'em coming!)

* reformat some code to use Jon Sterling Thought

* progress toward super advanced restriction-oriented elaborator

* explain Evan's other example

* rename utility function

* don't let the user type in a restriction type

* tentative fancy printing of goals with restriction

* fix generation of tactics for missing cases in elim

* comment

* smart constructor to decrease some term annotation clutter

* minor cleanup

* better version of typechecking algorithm

* NO MORE MANUAL ETA EXPANSION!!!!

* cleanup examples

* adding a basic auto tactic

* oops, remove quit statement

* one more

* exercise eta and auto a little more

* Close #212; close #237

* cleanup refiner interface a little

* factor sigma-intro out of elaborator and into refiner

* automatically do sigma-intro in auto

* formatting

* Elaborator: don't invoke normalizer to apply frames to terms

* add more stuff to torus example, note bug #240

* Resolve #240

* add "normalize" command (/cc @mortberg)

* finish up proof of torus ~ s1 × s1

* add links to other versions of the proof

* resolve #238

* removing bad.red from source control

* Oops, my fix didn't work. Just disable strict composition for now.

* add a clarifying comment

* remove bad.red from makefile

J.red

@@ -6,44 +6,47 @@ let J
   (x : A) (p : Path _ a x)
   : C x p
   =
-  let ty : dim → type = λ i →
-    let h : dim → A = λ j →
-      comp 0 j a [
-      | i=0 ⇒ λ _ → a
-      | i=1 ⇒ λ k → p k
-      ]
-    in
-    C (h 1) (λ k → h k)
+  let ty : dim → type =
+    λ i →
+      let h : dim → A =
+        λ j →
+          comp 0 j a [
+          | i=0 ⇒ auto
+          | i=1 ⇒ p
+          ]
+      in
+      C (h 1) h
   in
   coe 0 1 d in ty
 
 let J/eq
   (A : type) (a : A)
-  (C : (x : A) (p : Path A a x) → type) (d : C a (λ _ → a))
-  : Path (C a _) (J _ _ C d _ (λ _ → a)) d
+  (C : (x : A) (p : Path A a x) → type) (d : C a auto)
+  : Path (C a auto) (J _ _ C d _ (λ _ → a)) d
   =
   let square : dim → dim → A =
     λ i j →
       comp 0 j a [
-      | i=0 ⇒ λ _ → a
-      | i=1 ⇒ λ _ → a
+      | i=0 ⇒ auto
+      | i=1 ⇒ auto
       ]
   in
   λ k →
     comp 0 1 d in λ i →
       let aux : dim → A =
         λ j →
           comp 0 j a [
-          | k=0 ⇒ λ l → square i l
-          | k=1 ⇒ λ _ → a
-          | i=0 ⇒ λ _ → a
-          | i=1 ⇒ λ _ → a
+          | k=0 ⇒ square i
+          | k=1 ⇒ auto
+          | i=0 ⇒ auto
+          | i=1 ⇒ auto
           ]
       in
-      C (aux 1) (λ l → aux l)
+      C (aux 1) aux
     with
-    | k=0 ⇒ λ i →
-      coe 0 i d in λ j →
-        C (square j 1) (λ k → square j k)
-    | k=1 ⇒ λ _ → d
+    | k=0 ⇒
+      λ i →
+        coe 0 i d in λ j →
+          C (square j 1) (square j)
+    | k=1 ⇒ auto
     end

README.md

@@ -31,7 +31,7 @@ and [cubicaltt](https://github.com/mortberg/cubicaltt).
   supported)  based on the [work of Evan Cavallo and Bob
   Harper](https://arxiv.org/abs/1801.01568)
 
-- experimental support for Fitch-style modal guarded recursion: □, ▷
+- experimental support for Fitch-style modal guarded recursion: ▷
 
 
 Features we intend to add in the near future:

bool.red

@@ -15,6 +15,6 @@ let not∘not (x : bool) : _ =
 
 let not∘not/id/pt (x : bool) : Path _ (not∘not x) x =
   elim x [
-  | tt ⇒ λ _ → tt
-  | ff ⇒ λ _ → ff
+  | tt ⇒ auto
+  | ff ⇒ auto
   ]

connection.red

@@ -1,10 +1,5 @@
 import path
 
-let singleton (A : type) (M : A) : type pre =
-  restrict A [
-  | 0=0 ⇒ M
-  ]
-
 let connection/or
  (A : type)
  (p : dim → A)
@@ -22,27 +17,18 @@ let connection/or
   let face : dim → dim → A =
     λ l k →
       comp 0 l (p k) [
-      | k=1 ⇒ λ _ → p 1
-      | k=0 ⇒ λ m → p m
+      | k=1 ⇒ auto
+      | k=0 ⇒ p
       ]
   in
   comp 1 0 (p 1) [
-  | i=0 ⇒ λ k → face j k
-  | i=1 ⇒ λ k → face 1 k
-  | j=0 ⇒ λ k → face i k
-  | j=1 ⇒ λ k → face 1 k
-  | i=j ⇒ λ k → face i k
+  | i=0 ⇒ face j
+  | i=1 ⇒ face 1
+  | j=0 ⇒ face i
+  | j=1 ⇒ face 1
+  | i=j ⇒ face i
   ]
 
-; an example of using the singleton type to establish an exact equality
-let connection/or/diagonal
- (A : type)
- (p : dim → A)
- : singleton _ p
- =
- λ i →
-   connection/or _ p i i
-
 let connection/and
  (A : type)
  (p : dim → A)
@@ -57,16 +43,16 @@ let connection/and
    let face : dim → dim → A =
      λ l k →
        comp 1 l (p k) [
-       | k=0 ⇒ λ _ → p 0
-       | k=1 ⇒ λ m → p m
+       | k=0 ⇒ auto
+       | k=1 ⇒ p
        ]
    in
    comp 0 1 (p 0) [
-   | i=0 ⇒ λ k → face 0 k
-   | i=1 ⇒ λ k → face j k
-   | j=0 ⇒ λ k → face 0 k
-   | j=1 ⇒ λ k → face i k
-   | i=j ⇒ λ k → face i k
+   | i=0 ⇒ face 0
+   | i=1 ⇒ face j
+   | j=0 ⇒ face 0
+   | j=1 ⇒ face i
+   | i=j ⇒ face i
    ]
 
 

equivalence.red

@@ -15,3 +15,8 @@ let IsEquiv (A, B : type) (f : A → B) : type =
 
 let Equiv (A, B : type) : type =
   (f : A → B) × IsEquiv _ _ f
+
+let UA (A,B : type) (E : Equiv A B) : Path^1 type A B =
+  λ i →
+    `(V i A B E)
+

hedberg-wip.red

@@ -23,10 +23,9 @@ let or/elim
   (m0 : A → C)
   (m1 : B → C)
   : C =
-  sg/elim bool (λ b → elim b [tt ⇒ A | ff ⇒ B]) (λ _ _ → C) t
+  sg/elim bool _ (λ _ _ → C) t
     (λ b →
-      elim b in (λ b → (elim b in (λ _ → type) [tt ⇒ A | ff ⇒ B]) → C)
-      [tt ⇒ m0 | ff ⇒ m1])
+      elim b [tt ⇒ m0 | ff ⇒ m1])
 
 let neg (A : type) : type =
   A → void

int.red

@@ -30,23 +30,23 @@ let isuc (x : int) : int =
 
 let pred-isuc (n : int) : Path int (pred (isuc n)) n =
   elim n [
-  | pos n ⇒ λ _ → pos n
+  | pos n ⇒ auto
   | negsuc n ⇒
     elim n [
-    | zero ⇒ λ _ → negsuc zero
-    | suc n ⇒ λ _ → negsuc (suc n)
+    | zero ⇒ auto
+    | suc n ⇒ auto
     ]
   ]
 
 let isuc-pred (n : int) : Path int (isuc (pred n)) n =
   elim n [
   | pos n ⇒
     elim n [
-    | zero ⇒ λ _ → pos zero
-    | suc n' ⇒ λ _ → pos (suc n')
+    | zero ⇒ auto
+    | suc n' ⇒ auto
     ]
-  | negsuc n ⇒ λ _ → negsuc n
+  | negsuc n ⇒ auto
   ]
 
 let isuc-equiv : Equiv int int =
-  Iso/Equiv _ _ < isuc, < pred, < isuc-pred, pred-isuc > > >
+  Iso/Equiv _ _ <isuc, <pred, <isuc-pred, pred-isuc>>>

invariance.red

@@ -27,11 +27,11 @@ let shannon (A : type) (f : bool → A) : bool → A =
 
 
 let shannon/path (A : type) (f : bool → A) : Path _ f (shannon A f) =
-  funext bool _ _ _
+  funext _ _ f (shannon A f)
     (λ b →
-      elim b in λ x → Path _ (f x) (shannon A f x) [
-      | tt ⇒ λ _ → f tt
-      | ff ⇒ λ _ → f ff
+      elim b [
+      | tt ⇒ auto
+      | ff ⇒ auto
       ])
 
 let fun-to-pair-is-equiv (A : type) : IsEquiv^1 (_ → _) _ (fun-to-pair A) =
@@ -45,8 +45,8 @@ let fun-to-pair-is-equiv (A : type) : IsEquiv^1 (_ → _) _ (fun-to-pair A) =
           >)
       in λ j →
         [i] (f : bool → A) × Path (A × A) <f tt, f ff> p [
-        | i=0 ⇒ < shannon/path A (fib.0) j, fib.1 >
-        | i=1 ⇒ < pair-to-fun A p, λ _ → p >
+        | i=0 ⇒ <shannon/path A (fib.0) j, fib.1>
+        | i=1 ⇒ <pair-to-fun A p, auto>
         ]
     >
 

isotoequiv.red

@@ -23,8 +23,8 @@ let Iso/fiber-is-prop
   let sq : (_ : Fiber _ _ (I.0) b) (i, j : dim) → A =
     λ fib i j →
       comp 0 j (g (fib.1 i)) [
-      | i=0 ⇒ λ k → β (fib.0) k
-      | i=1 ⇒ λ _ → g b
+      | i=0 ⇒ β (fib.0)
+      | i=1 ⇒ auto
       ]
   in
   λ fib0 fib1 →
@@ -36,21 +36,21 @@ let Iso/fiber-is-prop
         ]
     in
     λ i →
-     < sq2 i 0
+     < auto
      , λ j →
         let aux : A =
           comp 1 0 (sq2 i j) [
-          | i=0 ⇒ λ k → sq fib0 j k
-          | i=1 ⇒ λ k → sq fib1 j k
-          | j=0 ⇒ λ k → β (sq2 i 0) k
-          | j=1 ⇒ λ _ → g b
+          | i=0 ⇒ sq fib0 j
+          | i=1 ⇒ sq fib1 j
+          | j=0 ⇒ β (sq2 i 0)
+          | j=1 ⇒ auto
           ]
         in
         comp 0 1 (f aux) [
-        | i=0 ⇒ λ k → α (fib0.1 j) k
-        | i=1 ⇒ λ k → α (fib1.1 j) k
-        | j=0 ⇒ λ k → α (f (sq2 i 0)) k
-        | j=1 ⇒ λ k → α b k
+        | i=0 ⇒ α (fib0.1 j)
+        | i=1 ⇒ α (fib1.1 j)
+        | j=0 ⇒ α (f (sq2 i 0))
+        | j=1 ⇒ α b
         ]
      >
 

modal.red

@@ -30,57 +30,3 @@ let stream/tl (xs : stream) : ✓ → stream =
 let tts : _ =
   fix xs : stream in
     stream/cons tt xs
-
-
-; To eliminate a box, write 'b !'; this elaborates to the core term `(open b).
-let bool/constant (x : bool) : (b : □ bool) × Path _ x (b !) =
-  elim x [
-  | tt ⇒ < shut tt, λ _ → tt >
-  | ff ⇒ < shut ff, λ _ → ff >
-  ]
-
-let sequence : type = □ stream
-
-
-let Next (A : type) (x : A) ✓ : A =
-  x
-
-let sequence/cons (x : bool) (xs : sequence) : sequence =
-  shut
-    stream/cons
-      (bool/constant x .0 !)
-      (Next stream (xs !))
-      ; this is suspicious: we use this Next in order to essentially
-      ; weaken away the tick that we will not use, in order to get the right number
-      ; of locks deleted. But this is proof-theoretically very strange.
-
-; The proper solution to the problem above is to bind lock names in the syntax and in the context,
-; analogous to tick names. This will make the calculus more baroque, but it will enable a
-; deterministic version of the 'open' rule. The source term for the above would then be:
-;
-;     λ α → stream/cons (bool/constant x .0 α) (λ β → xs α)
-;
-; Above, α is a lock name and β is a tick name; opening with the lock α
-; would *delete* the tick β from the context (thinking backward), which is
-; a tick weakening. the example would typecheck because there is no need for
-; β in xs.
-;
-; For reference, the core-language term would look like the following:
-;
-;    (shut [α]
-;     (stream/cons
-;      (open α (car (bool/constant x)))
-;      (next [β] (open α xs))))
-
-
-
-let sequence/hd (xs : sequence) : bool =
-  stream/hd (xs !)
-
-let sequence/tl (xs : sequence) : sequence =
-  shut
-    stream/tl (xs !) ∙
-
-
-let law/k (A,B : type) (f : □ (A → B)) (x : □ A) : □ B =
-  shut f ! (x !)

nat.red

@@ -13,7 +13,7 @@ let nat-pred (x : nat) : nat =
 
 
 let nat-pred/suc (x : nat) : Path nat x (nat-pred (suc x)) =
-  λ _ → x
+  auto
 
 let plus : nat → nat → nat =
   λ m n →
@@ -23,23 +23,23 @@ let plus : nat → nat → nat =
     ]
 
 let plus/unit/l (n : nat) : Path nat (plus zero n) n =
-  λ i → n
+  auto
 
 let plus/unit/r (n : nat) : Path nat (plus n zero) n =
   elim n [
-  | zero ⇒ λ _ → zero
+  | zero ⇒ auto
   | suc (n ⇒ path/n) ⇒ λ i → suc (path/n i)
   ]
 
 let plus/assoc (n : nat) : (m, o : nat) → Path nat (plus n (plus m o)) (plus (plus n m) o) =
   elim n [
-  | zero ⇒ λ m o i → plus m o
+  | zero ⇒ auto
   | suc (n ⇒ plus/assoc/n) ⇒ λ m o i → suc (plus/assoc/n m o i)
   ]
 
 let plus/suc/r (n : nat) : (m : nat) → Path nat (plus n (suc m)) (suc (plus n m)) =
   elim n [
-  | zero ⇒ λ m _ → suc m
+  | zero ⇒ auto
   | suc (n ⇒ plus/n/suc/r) ⇒ λ m i → suc (plus/n/suc/r m i)
   ]