Skip to content

Instantly share code, notes, and snippets.

@ikedaisuke

ikedaisuke/gist:1344227

Created November 7, 2011 05:12
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save ikedaisuke/1344227 to your computer and use it in GitHub Desktop.
Save ikedaisuke/1344227 to your computer and use it in GitHub Desktop.
Download ZIP
Thierry's proof of the principle of infinite descent (a part) in Agda2
Raw
gistfile1.txt
infiniteDescent : ∀ {a l} -> (A : Set a) -> (R : Rel A l) ->
(P : Pred A l) -> Noether A R ->
((x : A) -> P x -> ∃ (λ y -> R y x × P y)) ->
(z : A) -> ¬ (P z)
infiniteDescent A R P noe f
= noe (λ w → ¬ P w) g
where g : (x : A) → ((y : A) → R y x → ¬ P y) → ¬ P x
g x h px with f x px
... | (v , k) = h v (proj₁ k) (proj₂ k)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment