From 4611b121126c55bf32bf8fc89a9258cbb2337aa7 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 18 Jul 2016 11:55:38 -0700 Subject: Add natsimplify lemmas about eq_nat_dec --- src/Util/NatUtil.v | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) (limited to 'src/Util/NatUtil.v') diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v index 6d4efd9f4..4800ecb95 100644 --- a/src/Util/NatUtil.v +++ b/src/Util/NatUtil.v @@ -207,3 +207,31 @@ Proof. Qed. Hint Rewrite eq_nat_dec_refl : natsimplify. + +(** Helper to get around the lack of function extensionality *) +Definition eq_nat_dec_right_val n m (pf0 : n <> m) : { pf | eq_nat_dec n m = right pf }. +Proof. + revert dependent n; induction m; destruct n as [|n]; simpl; + intro pf0; + [ (exists pf0; exfalso; abstract congruence) + | eexists; reflexivity + | eexists; reflexivity + | ]. + { specialize (IHm n (fun e => pf0 (f_equal_nat nat S n m e))). + destruct IHm as [? IHm]. + eexists; rewrite IHm; reflexivity. } +Qed. + +Lemma eq_nat_dec_S_n n : eq_nat_dec (S n) n = right (proj1_sig (@eq_nat_dec_right_val _ _ (@neq_succ_diag_l n))). +Proof. + edestruct eq_nat_dec_right_val; assumption. +Qed. + +Hint Rewrite eq_nat_dec_S_n : natsimplify. + +Lemma eq_nat_dec_n_S n : eq_nat_dec n (S n) = right (proj1_sig (@eq_nat_dec_right_val _ _ (n_Sn n))). +Proof. + edestruct eq_nat_dec_right_val; assumption. +Qed. + +Hint Rewrite eq_nat_dec_n_S : natsimplify. -- cgit v1.2.3