Skip to content

Instantly share code, notes, and snippets.

@Lysxia

Lysxia/pacodep.v

Created May 22, 2019 00:15
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 Lysxia/6575548953eb25dadb07b15ea766ed69 to your computer and use it in GitHub Desktop.
Save Lysxia/6575548953eb25dadb07b15ea766ed69 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
pacodep.v
Require Import Paco.paco.
Module KO.
Definition test A (r : A -> Prop) : A -> Prop := fun _ => False.
Definition ptest A : A -> Prop := paco1 (test A) bot1.
Goal forall (A : Type) (l : A),
ptest A l.
Proof.
Fail pcofix CIH.
Abort.
End KO.
Module OK.
Definition test (r : forall A, A -> Prop) : forall A, A -> Prop := fun _ _ => False.
Definition ptest : forall A, A -> Prop := paco2 test bot2.
Goal forall (A : Type) (l : A),
ptest A l.
Proof.
pcofix CIH.
Abort.
End OK.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment