Skip to content

Instantly share code, notes, and snippets.

@Blaisorblade

Blaisorblade/int_eq.v

Last active January 28, 2020 00:33
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 Blaisorblade/7a984acd822846a486adf59e25129e8b to your computer and use it in GitHub Desktop.
Save Blaisorblade/7a984acd822846a486adf59e25129e8b to your computer and use it in GitHub Desktop.
Download ZIP
How to prove equality of sigma types with decidable predicates
Raw
int_eq.v
From mathcomp Require Import ssreflect ssrnat eqtype ssrbool seq tuple.
Import EqNotations.
Lemma sig_bool_eq {A : Type} {P : A -> bool} (x y: {z | P z}): sval x = sval y -> x = y.
Proof.
case: x y => [x Px] [y Py] /= Hxy; destruct Hxy.
apply eq_exist_uncurried. exists (Logic.eq_refl _).
apply bool_irrelevance.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment