Proof_of_plebeia_hash_calculation.v

Require Import List.
Import ListNotations.

Lemma fst_injective : forall {A B: Type} (p1 p2: A * B),
    fst p1 <> fst p2 -> p1 <> p2.
Proof.
  intros A B p1 p2. destruct p1, p2. simpl. intros Ha Hp.
  elim Ha. now injection Hp.
Qed.

Parameter hash : Set.
Parameter zerohash : hash.
Parameter hash_neq_bool : hash -> hash -> bool.
(*Axiom hash_neq_bool_refl : forall h, hash_neq_bool h h = false.*)
Declare Scope hash_scope.
Delimit Scope hash_scope with hash.
Infix "<>?" := hash_neq_bool (at level 60) : hash_scope.

Parameter segment : Set.
Parameter zerosegment : segment.
Parameter segment_neq_bool : segment -> segment -> bool.
Axiom segment_neq_bool_refl : forall s, segment_neq_bool s s = false.
Declare Scope segment_scope.
Delimit Scope segment_scope with segment.
Infix "<>?" := segment_neq_bool (at level 60) : segment_scope.

Definition hash_segment : Set := (hash * segment).
Definition zerohs : hash_segment := (zerohash, zerosegment).

Parameter value : Set.
Parameter hash_of_value : value -> hash.
Axiom hash_of_value_injective : forall v1 v2,
    v1 <> v2 -> hash_of_value v1 <> hash_of_value v2.
Axiom hash_of_value_injective_contr : forall v1 v2,
    hash_of_value v1 = hash_of_value v2 -> v1 = v2.
Axiom hash_of_value_nonzero : forall v,
    hash_of_value v <> zerohash.

Inductive node : Set :=
  | Leaf : value -> node
  | Bud : option node -> node
  | Internal : node -> node -> node
  | Extender : segment -> node -> node.

Check node_ind.

Fixpoint node_ind' (P : node -> Prop)
         (Case1 : forall v : value, P (Leaf v))
         (Case2 : P (Bud None))
         (Case3 : forall n : node, P n -> P (Bud (Some n)))
         (Case4 : forall n1, P n1 -> forall n2, P n2 -> P (Internal n1 n2))
         (Case5 : forall (s : segment) (n : node), P n -> P (Extender s n))
         (n : node) : P n :=
  match n with
  | Leaf v => Case1 v
  | Bud None => Case2
  | Bud (Some n) => Case3 n (node_ind' P Case1 Case2 Case3 Case4 Case5 n)
  | Internal n1 n2 => Case4 n1 (node_ind' P Case1 Case2 Case3 Case4 Case5 n1)
                            n2 (node_ind' P Case1 Case2 Case3 Case4 Case5 n2)
  | Extender seg n => Case5 seg n (node_ind' P Case1 Case2 Case3 Case4 Case5 n)
  end.

Parameter merge : list hash_segment -> hash.

(** invariant for merge

   forall hash_segment1, hash_segment2, hash_segment3, hash_segment4,
   if (hash_segment1, hash_segment2) <> (hash_segment3, hash_segment4),
   merge (hash_segment1, hash_segment2) <> merge (hash_segment3, hash_segment4)
*)

Axiom merge_injective_contr :
   forall hash_segments1 hash_segments2,
     merge hash_segments1 = merge hash_segments2 ->
     List.Forall2 (eq) hash_segments1 hash_segments2.
Axiom merge_nonzero : forall hslist, merge hslist <> zerohash.

Axiom merge_hash_of_value_not_collide : forall hslist v,
    hash_of_value v <> merge hslist.

Fixpoint h node :=
  match node with
  | Leaf v => (hash_of_value v, zerosegment)
  | Bud None => (zerohash, zerosegment)
  | Bud (Some n) => (merge [h n], zerosegment)
  | Internal n1 n2 => (merge [h n1; h n2], zerosegment)
  | Extender seg n => (fst (h n), seg)
  end.

(*let rec invariant_node = function
  | Leaf hash -> hash <> zerohash
  | Extender (segment, Extender _) -> false
  | Extender (segment, n) ->
      segment <> zerosegment
      && invariant_node n
  | Internal (n1, n2) -> invariant_node n1 && invariant_node n2
*)

Fixpoint invariant_node node :=
  match node with
  | Leaf v => (hash_of_value v <>? zerohash)%hash
  | Bud None => true
  | Bud (Some n) => invariant_node n
  | Extender segment (Extender _ _) => false
  | Extender segment n =>
    ((segment <>? zerosegment)%segment
      && invariant_node n)%bool
  | Internal n1 n2 => (invariant_node n1 && invariant_node n2)%bool
  end.

Definition Invariant node :=
  invariant_node node = true.

Lemma Invariant_inv_Bud : forall n,
    Invariant (Bud (Some n)) ->
    Invariant n.
Proof.
  now unfold Invariant.
Qed.

Lemma Invariant_inv_Extender : forall seg n,
    Invariant (Extender seg n) ->
    Invariant n.
Proof.
  intros seg n. unfold Invariant. simpl.
  intro eq.
  cut ((seg <>? zerosegment)%segment && invariant_node n = true)%bool.
  - intros Hseg. now rewrite Bool.andb_true_iff in Hseg.
  - now destruct n.
Qed.

Lemma Invariant_inv_Internal : forall n1 n2,
    Invariant (Internal n1 n2) ->
    Invariant n1 /\ Invariant n2.
Proof.
  intros n1 n2. unfold Invariant. simpl. intro and.
  now apply Bool.andb_true_iff.
Qed.

Hint Resolve merge_hash_of_value_not_collide : core.
Hint Resolve hash_of_value_injective_contr : core.

Ltac t1 eq := simpl; injection 1 as eq; eelim merge_hash_of_value_not_collide;
              (rewrite eq || rewrite <- eq).
Ltac t2 eq := simpl; injection 1 as eq; eelim hash_of_value_nonzero;
              (rewrite eq || rewrite <- eq).
Ltac t3 eq := simpl; injection 1 as eq; eelim merge_nonzero;
              (rewrite eq || rewrite <- eq).
Ltac myauto Heq := solve [now t2 Heq | now t1 Heq | now t3 Heq].


Lemma Forall2_one : forall {A B: Type} (P : A -> B -> Prop) x y,
    Forall2 P [x] [y] -> P x y.
Proof.
  intros A B P x y H. now inversion H.
Qed.


Lemma hash_inj_Leaf_Bud : forall v o,
    h (Leaf v) <> h (Bud o).
Proof.
  destruct o; simpl; now myauto Heq.
Qed.

Lemma hash_inj_Leaf_Internal : forall v n1 n2,
    h (Leaf v) <> h (Internal n1 n2).
Proof.
  intros v n1 n2. now myauto Heq.
Qed.

Lemma hash_inj_Leaf_Extender : forall v seg n,
    Invariant (Extender seg n) ->
    h (Leaf v) <> h (Extender seg n).
Proof.
  intros v seg n Inv. simpl.
  injection 1 as _ Hseg.
  unfold Invariant in Inv. simpl in Inv.
  rewrite Hseg, segment_neq_bool_refl in Inv. simpl in Inv.
  destruct n; discriminate Inv.
Qed.

Lemma hash_inj_Bud_Internal : forall o n1 n2,
    h (Bud o) <> h (Internal n1 n2).
Proof.
  intros o n1 n2. destruct o; try myauto Heq.
  simpl. injection 1 as Heq.
  apply merge_injective_contr in Heq. inversion Heq. inversion H4.
Qed.

Lemma hash_inj_Bud_Extender : forall o seg n,
    Invariant (Extender seg n) ->
    h (Bud o) <> h (Extender seg n).
Proof.
  intros o seg n Inv. unfold Invariant in Inv. simpl in Inv.
  simpl. intro Heq.
  cut (seg = zerosegment).
  - intro Hseg. rewrite Hseg, segment_neq_bool_refl in Inv. simpl in Inv.
    destruct n; discriminate Inv.
  - destruct o; now injection Heq.
Qed.

Lemma hash_inj_Internal_Extender : forall n1 n2 seg n,
    Invariant (Extender seg n) ->
    h (Internal n1 n2) <> h (Extender seg n).
Proof.
  intros n1 n2 seg n Inv.
  simpl. injection 1 as _ Hseg.
  unfold Invariant in Inv. simpl in Inv.
  rewrite Hseg, segment_neq_bool_refl in Inv. simpl in Inv.
  now destruct n.
Qed.

Lemma hash_extender : forall seg n,
  Invariant (Extender seg n) ->
  exists hash, h n = (hash, zerosegment).
Proof.
  intros seg n. unfold Invariant. destruct n; simpl.
  - now exists (hash_of_value v).
  - destruct o.
    + now exists (merge [h n]).
    + now exists zerohash.
  - now exists (merge [h n1; h n2]).
  - discriminate.
Qed.

(* Theorem

   forall n1, n2, if n1 <> n2, h(n1) <> h(n2)
*)
Theorem hash_injective : forall n1 n2,
    Invariant n1 -> Invariant n2 ->
    n1 <> n2 -> h n1 <> h n2.
Proof.
  induction n1 using node_ind'; destruct n2; intros Inv1 Inv2 Hneq.
  - (* Leaf, Leaf *)
    simpl. injection 1 as Heq. elim Hneq. f_equal.
    now apply hash_of_value_injective_contr.
  - now apply hash_inj_Leaf_Bud.
  - now apply hash_inj_Leaf_Internal.
  - now apply hash_inj_Leaf_Extender.
  - now apply not_eq_sym, hash_inj_Leaf_Bud.
  - (* Bud None, Bud *)
    destruct o; simpl; [myauto Heq|].
    now elim Hneq.
  - now apply hash_inj_Bud_Internal.
  - now apply hash_inj_Bud_Extender.
  - now apply not_eq_sym, hash_inj_Leaf_Bud.
  - (* Bud Some, Bud *)
    destruct o; simpl; [| myauto Heq].
    injection 1 as Heq. elim (IHn1 n).
    + now apply Invariant_inv_Bud.
    + now apply Invariant_inv_Bud.
    + intro Heqn. elim Hneq. now do 2 f_equal.
    + apply Forall2_one.
      now apply merge_injective_contr.
  - now apply hash_inj_Bud_Internal.
  - now apply hash_inj_Bud_Extender.
  - now apply not_eq_sym, hash_inj_Leaf_Internal.
  - now apply not_eq_sym, hash_inj_Bud_Internal.
  - (* Internal, Internal *)
    simpl. injection 1 as Heq.
    apply merge_injective_contr in Heq.
    inversion Heq as [| _hs1 _hs2 _l _l' Heqh1 Heqh2].
    apply Forall2_one in Heqh2. subst _hs1 _hs2 _l _l'.
    destruct (IHn1_1 n2_1); [now apply (Invariant_inv_Internal n1_1 n1_2)
                            | now apply (Invariant_inv_Internal n2_1 n2_2)
                            | | now apply Heqh1].
    intro Heq1.
    destruct (IHn1_2 n2_2); [now apply (Invariant_inv_Internal n1_1 n1_2)
                            | now apply (Invariant_inv_Internal n2_1 n2_2)
                            | | now apply Heqh2]. intro Heq2.
    elim Hneq. now subst n1_1 n1_2.
  - now apply hash_inj_Internal_Extender.
  - now apply not_eq_sym, hash_inj_Leaf_Extender.
  - now apply not_eq_sym, hash_inj_Bud_Extender.
  - now apply not_eq_sym, hash_inj_Internal_Extender.
  - (* Extender, Extender *)
    simpl. injection 1 as Hhash Hseg.
    destruct (hash_extender _ _ Inv1) as [h1 Hn1].
    destruct (hash_extender _ _ Inv2) as [h2 Hn2].
    rewrite Hn1, Hn2 in Hhash. simpl in Hhash.
    destruct (IHn1 n2).
    + now apply (Invariant_inv_Extender s n1).
    + now apply (Invariant_inv_Extender s0 n2).
    + intro H_child.
      elim Hneq. now rewrite H_child, Hseg.
    + now rewrite Hn1, Hn2, Hhash.
Qed.

改良版

Require Import List.
Import ListNotations.

Lemma fst_injective : forall {A B: Type} (p1 p2: A * B),
    fst p1 <> fst p2 -> p1 <> p2.
Proof.
  intros A B p1 p2. destruct p1, p2. simpl. intros Ha Hp.
  elim Ha. now injection Hp.
Qed.

Parameter hash : Set.
Parameter zerohash : hash.
Parameter hash_neq_bool : hash -> hash -> bool.
(*Axiom hash_neq_bool_refl : forall h, hash_neq_bool h h = false.*)
Declare Scope hash_scope.
Delimit Scope hash_scope with hash.
Infix "<>?" := hash_neq_bool (at level 60) : hash_scope.

Parameter segment : Set.
Parameter zerosegment : segment.
Parameter segment_neq_bool : segment -> segment -> bool.
Axiom segment_neq_bool_refl : forall s, segment_neq_bool s s = false.
Declare Scope segment_scope.
Delimit Scope segment_scope with segment.
Infix "<>?" := segment_neq_bool (at level 60) : segment_scope.

Definition hash_segment : Set := (hash * segment).
Definition zerohs : hash_segment := (zerohash, zerosegment).

Parameter value : Set.
Parameter hash_of_value : value -> hash.
Axiom hash_of_value_injective : forall v1 v2,
    v1 <> v2 -> hash_of_value v1 <> hash_of_value v2.
Axiom hash_of_value_injective_contr : forall v1 v2,
    hash_of_value v1 = hash_of_value v2 -> v1 = v2.
Axiom hash_of_value_nonzero : forall v,
    hash_of_value v <> zerohash.

Parameter index : Set.

Inductive node : Set :=
  | Disk : index -> node
  | View : view -> node
with view : Set :=
  | Leaf : value -> view
  | Bud : option node -> view
(*  | Internal : node -> node -> node
  | Extender : segment -> node -> node.*)
.

Check node_ind.

Scheme node_view_ind := Induction for node Sort Prop
with view_node_ind := Induction for view Sort Prop.

Check node_view_ind.

Parameter load : index -> view.
Definition view_of_node node :=
  match node with
  | Disk i => load i
  | View v => v
  end.

Inductive node_eq : node -> node -> Prop :=
| NodeEq : forall n1 n2,
    view_eq (view_of_node n1) (view_of_node n2) ->
    node_eq n1 n2
with view_eq : view -> view -> Prop :=
| LeafEq : forall value, view_eq (Leaf value) (Leaf value)
| BudNoneEq : view_eq (Bud None) (Bud None)
| BudSomeEq : forall n1 n2,
    node_eq n1 n2 -> view_eq (Bud (Some n1)) (Bud (Some n2))
.

Hint Constructors node_eq view_eq.

Parameter size_of_node : node -> nat.

Fixpoint size_of_view v :=
  match v with
  | Leaf _ => 1
  | Bud None => 0
  | Bud (Some n) => 1 + size_of_node n
  end.

Axiom size_of_node_Disk : forall i,
    size_of_node (Disk i) = 1 + size_of_view (load i).
Axiom size_of_node_View : forall v,
    size_of_node (View v) = 1 + size_of_view v.

Section NodeRect.

  Variable Pv : view -> Type.
  Variable Pn : node -> Type.

  Variable (CaseDisk : forall i, Pv (load i) -> Pn (Disk i)).
  Variable (CaseView : forall v, Pv v -> Pn (View v)).

  Variable (CaseLeaf : forall v : value, Pv (Leaf v)).
  Variable (CaseBudNone : Pv (Bud None)).
  Variable (CaseBudSome : forall n : node, Pn n -> Pv (Bud (Some n))).

  Definition node_view := sum node view.
  Definition size_of_nv nv :=
    sum_rec (Basics.const nat) size_of_node size_of_view nv.
  Definition Pnv nv :=
    match nv with
    | inl node => Pn node
    | inr view => Pv view
    end.

  Require Import Recdef.
  Function node_view_mut (nv : node_view) {measure size_of_nv nv} : Pnv nv :=
    match nv return Pnv nv with
    | inl (Disk i) => CaseDisk i (node_view_mut (inr (load i)))
    | inl (View v) => CaseView v (node_view_mut (inr v))
    | inr (Leaf value) => CaseLeaf value
    | inr (Bud None) => CaseBudNone
    | inr (Bud (Some n)) => CaseBudSome n (node_view_mut (inl n))
    end.
  - intros nv n i Hn Hnv. simpl. rewrite size_of_node_Disk. now auto.
  - intros nv n v Hn Hnv. simpl. rewrite size_of_node_View. now auto.
  - intros nv v o n Ho Hv Hnv. simpl. now auto.
  Defined.

  (*Print R_node_view_mut.*)

  Definition node_mut (n : node) : Pn n := node_view_mut (inl n).
  Definition view_mut (v : view) : Pv v := node_view_mut (inr v).

End NodeRect.

Parameter merge : list hash_segment -> hash.

(** invariant for merge

   forall hash_segment1, hash_segment2, hash_segment3, hash_segment4,
   if (hash_segment1, hash_segment2) <> (hash_segment3, hash_segment4),
   merge (hash_segment1, hash_segment2) <> merge (hash_segment3, hash_segment4)
*)

Axiom merge_injective_contr :
   forall hash_segments1 hash_segments2,
     merge hash_segments1 = merge hash_segments2 ->
     List.Forall2 (eq) hash_segments1 hash_segments2.
Axiom merge_nonzero : forall hslist, merge hslist <> zerohash.

Axiom merge_hash_of_value_not_collide : forall hslist v,
    hash_of_value v <> merge hslist.

Require Import Recdef.

Function h nv {measure size_of_nv nv} :=
  match nv with
  | inl (Disk i) => h (inr (load i))
  | inl (View v) => h (inr v)
  | inr (Leaf value) => (hash_of_value value, zerosegment)
  | inr (Bud None) => (zerohash, zerosegment)
  | inr (Bud (Some n)) => (merge [h (inl n)], zerosegment)
  end.
- intros nv n i Hn Hnv. simpl. rewrite size_of_node_Disk. auto with arith.
- intros nv n v Hn Hnv. simpl. rewrite size_of_node_View. auto with arith.
- intros nv v o n Ho Hv Hnv. simpl. auto with arith.
Defined.

Definition hash_of_view v := h (inr v).
Definition hash_of_node n := h (inl n).

Lemma hash_of_node_equation : forall n,
    hash_of_node n = match n with
                     | Disk i => hash_of_view (load i)
                     | View v => hash_of_view v
                     end.
Proof.
  intros n. unfold hash_of_node. now rewrite h_equation.
Qed.

Lemma hash_of_view_equation : forall v,
  hash_of_view v = match v with
                   | Leaf value => (hash_of_value value, zerosegment)
                   | Bud None => (zerohash, zerosegment)
                   | Bud (Some n) => (merge [hash_of_node n], zerosegment)
                   end.
Proof.
  intros n. unfold hash_of_view. now rewrite h_equation.
Qed.

(*let rec invariant_node = function
  | Leaf hash -> hash <> zerohash
  | Extender (segment, Extender _) -> false
  | Extender (segment, n) ->
      segment <> zerosegment
      && invariant_node n
  | Internal (n1, n2) -> invariant_node n1 && invariant_node n2
*)

Inductive Invariant_view : view -> Prop :=
| IVLeaf : forall v, hash_of_value v <> zerohash -> Invariant_view (Leaf v)
| IVBudNone : Invariant_view (Bud None)
| IVBudSome : forall n, Invariant_node n -> Invariant_view (Bud (Some n))
with Invariant_node : node -> Prop :=
| INDisk : forall i, Invariant_view (load i) -> Invariant_node (Disk i)
| INView : forall v, Invariant_view v -> Invariant_node (View v)
.


(*Lemma Invariant_inv_Extender : forall seg n,
    Invariant (Extender seg n) ->
    Invariant n.
Proof.
  intros seg n. unfold Invariant. simpl.
  intro eq.
  cut ((seg <>? zerosegment)%segment && invariant_node n = true)%bool.
  - intros Hseg. now rewrite Bool.andb_true_iff in Hseg.
  - now destruct n.
Qed.

Lemma Invariant_inv_Internal : forall n1 n2,
    Invariant (Internal n1 n2) ->
    Invariant n1 /\ Invariant n2.
Proof.
  intros n1 n2. unfold Invariant. simpl. intro and.
  now apply Bool.andb_true_iff.
Qed.*)

Ltac t1 eq := simpl; injection 1 as eq; eelim merge_hash_of_value_not_collide;
              (rewrite eq || rewrite <- eq).
Ltac t2 eq := simpl; injection 1 as eq; eelim hash_of_value_nonzero;
              (rewrite eq || rewrite <- eq).
Ltac t3 eq := simpl; injection 1 as eq; eelim merge_nonzero;
              (rewrite eq || rewrite <- eq).
Ltac myauto Heq := solve [now t2 Heq | now t1 Heq | now t3 Heq].


Lemma Forall2_one : forall {A B: Type} (P : A -> B -> Prop) x y,
    Forall2 P [x] [y] -> P x y.
Proof.
  intros A B P x y H. now inversion H.
Qed.


Lemma hash_inj_Leaf_Bud : forall v o,
    hash_of_view (Leaf v) <> hash_of_view (Bud o).
Proof.
  unfold hash_of_view. intros v o. do 2 rewrite h_equation.
  destruct o; simpl; now myauto Heq.
Qed.

Lemma hash_inj_Bud_None_Some : forall n,
    hash_of_view (Bud None) <> hash_of_view (Bud (Some n)).
Proof.
  intros n. do 2 rewrite hash_of_view_equation.
  now myauto Heq.
Qed.

(*Lemma hash_inj_Leaf_Internal : forall v n1 n2,
    hash_of_view (Leaf v) <> h (Internal n1 n2).
Proof.
  intros v n1 n2. now myauto Heq.
Qed.

Lemma hash_inj_Leaf_Extender : forall v seg n,
    Invariant (Extender seg n) ->
    h (Leaf v) <> h (Extender seg n).
Proof.
  intros v seg n Inv. simpl.
  injection 1 as _ Hseg.
  unfold Invariant in Inv. simpl in Inv.
  rewrite Hseg, segment_neq_bool_refl in Inv. simpl in Inv.
  destruct n; discriminate Inv.
Qed.

Lemma hash_inj_Bud_Internal : forall o n1 n2,
    h (Bud o) <> h (Internal n1 n2).
Proof.
  intros o n1 n2. destruct o; try myauto Heq.
  simpl. injection 1 as Heq.
  apply merge_injective_contr in Heq. inversion Heq. inversion H4.
Qed.

Lemma hash_inj_Bud_Extender : forall o seg n,
    Invariant (Extender seg n) ->
    h (Bud o) <> h (Extender seg n).
Proof.
  intros o seg n Inv. unfold Invariant in Inv. simpl in Inv.
  simpl. intro Heq.
  cut (seg = zerosegment).
  - intro Hseg. rewrite Hseg, segment_neq_bool_refl in Inv. simpl in Inv.
    destruct n; discriminate Inv.
  - destruct o; now injection Heq.
Qed.

Lemma hash_inj_Internal_Extender : forall n1 n2 seg n,
    Invariant (Extender seg n) ->
    h (Internal n1 n2) <> h (Extender seg n).
Proof.
  intros n1 n2 seg n Inv.
  simpl. injection 1 as _ Hseg.
  unfold Invariant in Inv. simpl in Inv.
  rewrite Hseg, segment_neq_bool_refl in Inv. simpl in Inv.
  now destruct n.
Qed.
*)
(*
Lemma hash_extender : forall seg n,
  Invariant (Extender seg n) ->
  exists hash, h n = (hash, zerosegment).
Proof.
  intros seg n. unfold Invariant. destruct n; simpl.
  - now exists (hash_of_value v).
  - destruct o.
    + now exists (merge [h n]).
    + now exists zerohash.
  - now exists (merge [h n1; h n2]).
  - discriminate.
Qed.*)

(* Theorem

   forall n1, n2, if n1 <> n2, h(n1) <> h(n2)
*)
Check node_mut.
Theorem hash_injective : forall n1 n2,
    Invariant_node n1 -> Invariant_node n2 ->
    ~ (node_eq n1 n2) -> hash_of_node n1 <> hash_of_node n2.
Proof.
  intros n1. eapply node_mut with (n := n1)
                                  (Pv := fun v1 => forall v2,
                                             Invariant_view v1 ->
                                                Invariant_view v2 ->
                                                ~ (view_eq v1 v2) ->
                                                hash_of_view v1 <> hash_of_view v2).
  - (* Disk *)
    intros i' IHv n2. do 2 rewrite hash_of_node_equation.
    intros Inv1 Inv2 Hneq.
    inversion Inv1. destruct n2.
    + inversion Inv2. apply IHv; try assumption.
      intro veq. now elim Hneq.
    + inversion Inv2. apply IHv; try assumption.
      intro veq. now elim Hneq.
  - (* View *)
    intros i IHv n2 Inv1 Inv2 Hneq. do 2 rewrite hash_of_node_equation.
    inversion Inv1. destruct n2.
    + inversion Inv2. apply IHv; try assumption.
      intro veq. now elim Hneq.
    + inversion Inv2. apply IHv; try assumption.
      intro veq. now elim Hneq.
  - (* Leaf v *)
    intros value v2 Inv1 Inv2 Hneq. destruct v2.
    + do 2 rewrite hash_of_view_equation.
      injection 1 as Heq.
      elim Hneq. now rewrite (hash_of_value_injective_contr _ _ Heq).
    + now apply hash_inj_Leaf_Bud.
  - (* Bud None *)
    intros v2 Inv1 Inv2 Hneq. destruct v2; [| destruct o].
    + now apply not_eq_sym, hash_inj_Leaf_Bud.
    + now apply hash_inj_Bud_None_Some.
    + now destruct Hneq.
  - (* Bud Some *)
    intros n1' IHv v2 Inv1 Inv2 Hneq. destruct v2; [| destruct o].
    + now apply not_eq_sym, hash_inj_Leaf_Bud.
    + do 2 rewrite hash_of_view_equation.
      injection 1 as Hmerge.
      apply merge_injective_contr in Hmerge.
      apply Forall2_one in Hmerge.
      inversion Inv1. inversion Inv2. subst n0 n2.
      destruct IHv with (n2 := n); try assumption. intro Heq.
      elim Hneq. now constructor.
    + now apply not_eq_sym, hash_inj_Bud_None_Some.
Qed.


Require Import Extraction.
Require Import ExtrOcamlBasic.
Extraction h.