{-# OPTIONS --cubical --safe #-} module 2019-4-21-CuttMltt where import Agda.Builtin.Equality as MLTT import Cubical.Core.Everything as CUTT import Agda.Builtin.Nat as MNat import Cubical.Data.Nat as CNat private variable A B : Set
In dependently-typed programming languages, we do equality proofs. Type Theory folks formed two groups; one stands for “proofs are not important”, one stands for “proofs are important”. Someone claims that the identity proof between two objects is unique – which is related to the K rule. The other people believe that the proof of identity is significant – the same theorem can have different proofs, where the identity relation on these proofs are also nontrivial and can be proved to be equivalent or not.
Intuitionistic Logic
First, let’s take a look at the world of unique identity proofs.
module Intuitionistic where open MLTT open MNat
In Intuitionistic Logic, we can prove new theorems via pattern matching on existing theorems, because identity proofs are instances of the equality type:
trans : {a b c : A} → a ≡ b → b ≡ c → a ≡ c trans refl refl = refl sym : {a b : A} → a ≡ b → b ≡ a sym refl = refl cong : {a b : A} → (f : A → B) → a ≡ b → f a ≡ f b cong _ refl = refl
or we can use rewrite
, which is syntactic sugar of pattern matching
(and this definition is more Idris style):
trans₁ : {a b c : A} → a ≡ b → b ≡ c → a ≡ c trans₁ p q rewrite p = q cong₁ : {a b : A} → (f : A → B) → a ≡ b → f a ≡ f b cong₁ _ p rewrite p = refl
These three functions, trans
, sym
and cong
are our equality proof
combinators.
Larger and more concrete theorems, such as the plus commutative law:
+-comm : ∀ a b → a + b ≡ b + a
can be proved by induction – the base case is simply a ≡ a + 0
,
where we can introduce a lemma for it:
+-comm zero b = +-zero b
… and we prove the lemma by induction as well:
where +-zero : ∀ a → a ≡ a + 0 +-zero zero = refl +-zero (suc a) = cong suc (+-zero a)
Very small theorems can be proved by induction trivially using
a recursive call as the induction hypothesis and let the cong
function to finish the induction step.
Combining induction and our trans
combinator we get the induction
step of the proof of the plus commutative law:
+-comm (suc a) b = trans (cong suc (+-comm a b)) (+-suc b a) where +-suc : ∀ a b → suc (a + b) ≡ a + suc b +-suc zero _ = refl +-suc (suc a) b = cong suc (+-suc a b)
On the other hand, even large theorems such as the plus commutative law
can also be proved without the help of lemmas.
Here’s an example, by exploiting the rewrite
functionality:
+-comm₁ : ∀ n m → n + m ≡ m + n +-comm₁ zero zero = refl +-comm₁ zero (suc m) rewrite sym (+-comm₁ zero m) = refl +-comm₁ (suc n) zero rewrite +-comm₁ n zero = refl +-comm₁ (suc n) (suc m) rewrite +-comm₁ n (suc m) | sym (+-comm₁ (suc n) m) | +-comm₁ n m = refl
What does rewrite
do?
Let’s look at it in detail.
To prove this theorem, whose goal is a + c ≡ b + d
,
step-by-step : ∀ {a b c d} → a ≡ b → c ≡ d → a + c ≡ b + d step-by-step {b = b} {d = d} p q
we first rewrite with p
, which turns the goal to b + c ≡ b + d
,
then rewrite with q
, which turns the goal to b + d ≡ b + d
,
rewrite p | q
which is a specialized version of refl
:
= refl {x = b + d}
It’s like we’re destructing our goal step by step and finally turn it into a specialized refl
.
For more complicated proofs, we’re not only destructing the goal – we’re also constructing
terms that can be used to destruct the goal.
rewrite
is how we use the constructed terms to destruct terms.
Our proof is bidirectional.
Cubical model
What if the identity proofs are not trivial?
module Cubical where open CUTT using (_≡_; I; ~_; hcomp; inS; hfill; i0; i1) open CNat
In the Cubical model, there’s no pattern matching because you can never tell
how many proofs there can be (so no case analysis).
Instead, there are interval operations that can construct proofs via existing proofs
in a more detailed way.
Inverting an interval is sym
:
sym : {a b : A} → a ≡ b → b ≡ a sym p i = p (~ i)
Creating a new interval by combining an old path with an arbitrary function
is cong
:
cong : {a b : A} (f : A → B) → a ≡ b → f a ≡ f b cong f p i = f (p i)
trans
is far more complicated – you’ll need cubical kan operation:
trans : {a b c : A} → a ≡ b → b ≡ c → a ≡ c trans p q i = hfill (λ { j (i = i0) → p i; j (i = i1) → q j}) (inS (p i)) i
Although we lose the ability to rewrite
, we still have our combinators – sym
, cong
and trans
,
which means that several existing proofs are still perfectly valid under the Cubical model.
On the other hand, according to the design of Path
types, some proofs become perfectly
natural. For instance, the step-by-step
theorem shown above can be proved by:
step-by-step : ∀ {a b c d} → a ≡ b → c ≡ d → a + c ≡ b + d step-by-step p q i = p i + q i
There can also be equality on functions, which is not even possible in the Intuitionistic type theory:
funExt : {f g : A → B} → (∀ x → f x ≡ g x) → f ≡ g funExt p i a = p a i
Obvious Conclusions
- The Cubical model introduces tons of primitives while it’s fairly more powerful than the Intuitionistic type theory
- Cubical model is harder implementation-wise
- Intuitionistic type theory is more friendly for letting the compiler to solve some unification problems
- Both of these two models are not gonna save Agda