Skip to content

Instantly share code, notes, and snippets.

@davidjao

davidjao/foo_rang_bar.v

Created April 22, 2023 03:51
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 davidjao/b6209fa5242368b80d77c996d7273600 to your computer and use it in GitHub Desktop.
Save davidjao/b6209fa5242368b80d77c996d7273600 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
foo_rang_bar.v
From Coq Require Import Utf8 ssreflect ssrbool ssrfun.
Parameter B : Type.
Parameter A : nat → Type.
Definition foo (n:nat) (a: A n) : B.
Proof.
admit.
Admitted.
Definition rang (b:B) : nat.
Proof.
admit.
Admitted.
Definition bar (b:B) : A (rang b).
Proof.
admit.
Admitted.
Theorem foo_rang_bar : ∀ (b:B), foo (rang b) (bar b) = b.
Proof.
admit.
Admitted.
Theorem rang_foo : ∀ (n:nat) (a: A n), rang (foo n a) = n.
Proof.
admit.
Admitted.
Definition cast {X Y : nat} (e : X = Y) : A X → A Y :=
match e with erefl => id end.
Goal ∀ (n:nat) (a: A n), cast (rang_foo _ _) (bar (foo n a)) = a.
Proof.
admit.
Admitted.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment