module 1Lab.Inductive where open import 1Lab.Reflection open import 1Lab.Equiv open import 1Lab.Type hiding (case_of_ ; case_return_of_) {- Automation for applying induction principles ============================================ When working with mixed truncations/products/quotients, the relevant induction principles are often repeatedly applied in close succession, like in the snippet below. □-rec! λ { (a , b , w) → □-rec! (λ { (c , d , x) → inc (c , d , inc (a , x , w)) }) b } Applying these induction principles is entirely mechanical: like other mechanical processes, it's annoying to do by hand, generates ugly code, and causes a deep sense of existential uselessness. This module implements automation for automatically applying these eliminators "as far as possible", using overlapping instances. The Inductive class ------------------- The core of the implementation for rec!/elim! is the Inductive class, which is a slight misnomer. To support *nested* types with a single constructor, the Inductive class is applied to a section of the motive, not just base type. That is, if we want to simplify □ (□ A × □ (□ A)) → B ^~~~~~~~~~~~~~~~~ domain we don't look for an instance of `Inductive domain`, we look for an instance of `Inductive (domain → B)`. The relevant instances then manipulate the entire function type at once, much like Extensional. Writing rules ------------- Like Extensional, instances of 'Inductive' should be maximally lazy, so that the structural rules can fire as often as possible. That is, instead of writing ⦃ _ : ∀ {x} → Inductive (P (inc x)) ⦄ → Inductive (∀ x → P x) we write ⦃ _ : Inductive (∀ x → P (inc x)) ⦄ → Inductive (∀ x → P x) -} record Inductive {ℓ} (A : Type ℓ) ℓm : Type (ℓ ⊔ lsuc ℓm) where field methods : Type ℓm from : methods → A open Inductive private variable ℓ ℓ' ℓ'' ℓm : Level A B C : Type ℓ P Q R : A → Type ℓ instance -- The basic structural rules allow us to stop recurring (we can -- produce an A given an A) and to skip an argument, introducing a -- function type into the methods: Inductive-default : Inductive A (level-of A) Inductive-default .methods = _ Inductive-default .from x = x Inductive-Π : ⦃ _ : {x : A} → Inductive (P x) ℓm ⦄ → Inductive (∀ x → P x) (level-of A ⊔ ℓm) Inductive-Π ⦃ r ⦄ .methods = ∀ x → r {x} .methods Inductive-Π ⦃ r ⦄ .from f x = r .from (f x) {-# INCOHERENT Inductive-default #-} {-# OVERLAPPABLE Inductive-Π #-} -- Next, we have a rule for uncurrying pairs. This lets us handle types like -- □ (□ A × □ B) → C -- -- by factoring through -- -- □ (□ A × □ B) → C -- □ A × □ B → C -- □ A → □ B → C -- □ B → C Inductive-Σ : ∀ {A : Type ℓ} {B : A → Type ℓ'} {C : (x : A) → B x → Type ℓ''} → ⦃ _ : Inductive ((x : A) (y : B x) → C x y) ℓm ⦄ → Inductive ((x : Σ A B) → C (x .fst) (x .snd)) ℓm Inductive-Σ ⦃ r ⦄ .methods = r .methods Inductive-Σ ⦃ r ⦄ .from f (x , y) = r .from f x y Inductive-Lift : {B : Lift ℓ A → Type ℓ'} → ⦃ _ : Inductive (∀ x → B (lift x)) ℓm ⦄ → Inductive (∀ x → B x) ℓm Inductive-Lift ⦃ i ⦄ = record { from = λ f (lift x) → i .from f x } -- However, we don't uncurry equivalences. Inductive-≃ : {C : A ≃ B → Type ℓ''} → Inductive (∀ x → C x) _ Inductive-≃ = Inductive-default {-# OVERLAPPING Inductive-≃ #-} -- There are two distinct prefix entry points: rec! and elim!. The -- difference is just in name, to provide a modicum of documentation. In -- addition, they have an explicit function type, so that the refine -- command will always introduce a question mark. rec! : ⦃ r : Inductive (A → B) ℓm ⦄ → r .methods → A → B rec! ⦃ r ⦄ = r .from elim! : ⦃ r : Inductive (∀ x → P x) ℓm ⦄ → r .methods → ∀ x → P x elim! ⦃ r ⦄ = r .from -- We also define versions of case_of_ and case_return_of_, shadowing -- those from 1Lab.Type, which insert a rec!/elim!. case_of_ : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} ⦃ r : Inductive (A → B) ℓm ⦄ → A → r .methods → B case x of f = rec! f x case_return_of_ : ∀ {ℓ ℓ'} {A : Type ℓ} (x : A) (B : A → Type ℓ') ⦃ r : Inductive (∀ x → B x) ℓm ⦄ (f : r .methods) → B x case x return P of f = elim! f x {-# INLINE case_of_ #-} {-# INLINE case_return_of_ #-}