Last active
January 21, 2020 19:59
-
-
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
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# 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