proposition: Lemma gss': forall (A: Type) opt (i: elt) (x: A) (m: ptrie A), wf opt m -> get' i (set' i x m) = Some x.
proof: Proof. induction 1; intros. - simpl. rewrite elt_eqb_refl; congruence. - simpl. destruct (elt_eqb i k) eqn:EQ; auto. + simpl. rewrite elt_eqb_refl. congruence. + unfold join. rewrite Key.eqb_false in EQ. generalize (Key.branching_bit_spec _ _ EQ). intros [m' [HA HB]]. case_eq (Key.zerobit i (Key.branching_bit i k)); intros; simpl; rewrite H; rewrite (elt_eqb_refl); congruence. - simpl. destruct (elt_eqb i k); auto. + simpl; rewrite elt_eqb_refl; congruence. + unfold join. case_eq (Key.zerobit i (Key.branching_bit i k)); intros; simpl; rewrite H; rewrite (elt_eqb_refl); congruence. - simpl. case_eq (Key.match_prefix i prefix brbit); intros. + case_eq (Key.zerobit i brbit); intros; simpl; rewrite H2; auto. + unfold join. case_eq (Key.zerobit i (Key.branching_bit i prefix)); intros; simpl; rewrite H2; rewrite (elt_eqb_refl); congruence. - simpl. case_eq (Key.match_prefix i prefix brbit); intros. + case_eq (Key.zerobit i brbit); intros; simpl; rewrite H2; auto. + unfold join. eapply Key.match_prefix_spec' in H1; auto. * destruct H1 as [HO [n [HA HB]]]. case_eq (Key.zerobit i (Key.branching_bit i prefix)); intros; simpl; rewrite H1; rewrite (elt_eqb_refl); congruence. * inv H; eauto; congruence. * inv H; eauto; congruence. Qed.
imports: Lia Cdcl.Coqlib