Skip to content

Instantly share code, notes, and snippets.

@gallais

gallais/Impredicative.v

Created February 14, 2018 16:51
Show Gist options
  • Star 1 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save gallais/fbba881e09aa349ea59093d8bbf153a4 to your computer and use it in GitHub Desktop.
Save gallais/fbba881e09aa349ea59093d8bbf153a4 to your computer and use it in GitHub Desktop.
Download ZIP
Using Impredicativity to beat the positivity checker
Raw
Impredicative.v
Inductive T :=
| Var : nat -> T
| App : T -> T -> T.
Inductive S e : Prop :=
| def: forall R, (forall i, R i -> S i) ->
(forall e', R e' -> S (App e e')) -> S e.
Definition def' :
forall e, (forall e', S e' -> S (App e e')) -> S e.
intros e ih; apply (def e S); auto.
Defined.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment