Skip to content

Instantly share code, notes, and snippets.

@pnlph
Last active January 21, 2020 19:59
Show Gist options
  • Save pnlph/d13253fffc34371e03eef8e14517ee5d to your computer and use it in GitHub Desktop.
Save pnlph/d13253fffc34371e03eef8e14517ee5d to your computer and use it in GitHub Desktop.
Function that takes an Enunciation and delivers its construction, last clause does not type check
{-# OPTIONS --without-K #-}
module Theorem where
------------------------------------------------------------------------
-- Definitions needed for Lemma 1.17
-- _≡_; sym; trans; cong; _≃_
------------------------------------------------------------------------
data _≡_ {A : Set} (x : A) : A → Set where
refl : x ≡ x
sym : {A : Set} {x y : A} → x ≡ y → y ≡ x
sym refl = refl
trans : {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans refl refl = refl
cong : {A B : Set} (f : A → B) {x y : A} → x ≡ y → f x ≡ f y
cong f refl = refl
record _≃_ (A B : Set) : Set where
field
apply : A → B
linv : B → A
rinv : B → A
isLinv : (x : A) → linv (apply x) ≡ x
isRinv : (y : B) → apply (rinv y) ≡ y
open _≃_
------------------------------------------------------------------------
-- Lemma 1.17
------------------------------------------------------------------------
-- Enunciation of lemma 1.17
lemma1-17 : Set₁
lemma1-17 = {A B : Set} (f : A ≃ B) (y : B) → linv f y ≡ rinv f y
-- Construction of lemma 1.17
linv-is-rinv : {A B : Set} (f : A ≃ B) (y : B) → linv f y ≡ rinv f y
linv-is-rinv f y = sym (trans (sym (isLinv f (rinv f y))) (cong (linv f) (isRinv f y)))
------------------------------------------------------------------------
-- Experimental
------------------------------------------------------------------------
-- Define record
--
record HasProof (X : Set₁) : Set₁ where
constructor [_]
field
theProof : X
-- Open record using instance arguments
-- implicit arguments resolved by a special instance resolution algorithm
open HasProof {{...}}
-- Nameless instance of lemma1-17 record
-- can only be referred to by instance search (i.e. through its type)
instance
_ : HasProof lemma1-17
-- 1. Verify the goal
-- 2. Find candidates
-- 3. Check the candidates
-- 4. Compute the result
_ = [ linv-is-rinv ]
-- Theorem
-- takes an enunciation X and delivers its proof theProof
th : (X : Set₁) {{_ : HasProof X}} -> X
th X = theProof
-- unnamed variable as proof
_ : lemma1-17
_ = th lemma1-17
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment