eponier

Require Import Coq.Lists.List.
Require Import Coq.Bool.Bool.
Import ListNotations.

Variant t := | a0 | a1.
Variant t2 : Type :=
| b0
| b1 `(t) `(t) `(t)
| b2 `(t)
| b3 `(t)

eponier

Lemma Add_transpose_neqkey : forall k1 k2 e1 e2 m1 m2 m3,
  ~ E.eq k1 k2 -> Add k1 e1 m1 m2 -> Add k2 e2 m2 m3 ->
  { m | Add k2 e2 m1 m /\ Add k1 e1 m m3 }.
Proof.
  intros k1 k2 e1 e2 m1 m2 m3 k_neq Add_1 Add_2.
  exists (add k2 e2 m1).
  split; [easy|].
  unfold Add; intros k.
  rewrite Add_2, add_o, Add_1, !add_o.
  destruct (eq_dec k1 k), (eq_dec k2 k); try reflexivity.

eponier

Require Import FMaps FMapFacts ZArith.

Module Import Test := Make (Z_as_OT).
Module Import P := Properties Test.

Module First_proof.

Lemma remove_In_Add : forall {A} k e (m : t A),
  MapsTo k e m ->
  Add k e (remove k m) m.

eponier

(* Answer to the challenge member_heq_eq of Gregory Malecha
   (https://gmalecha.github.io/reflections/2017/challenge-member_heq_eq)

   This answer is partly inspired from his own answer
   (https://gist.github.com/gmalecha/75c1577c2bed86e6d126859193909715)
*)

Require Import List. Import ListNotations.

Section del_val.