NodeHash.v

Require Import Premise.

Fixpoint hash node :=
  match node with
  | Bud None => zerohash
  | Bud (Some n) => h 2 (hash n)
  | Leaf v => h 0 (hash_of_value v)
  | Internal n1 n2 => h 1 (hash n1 ^^ hash n2)
  | Extender seg n => hash n ^^ seg
  end.

Fixpoint node_ind' (P : node -> Prop)
         (Case1 : P (Bud None))
         (Case2 : forall n : node, P n -> P (Bud (Some n)))
         (Case3 : forall v : value, P (Leaf v))
         (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
  | Bud None => Case1
  | Bud (Some n) => Case2 n (node_ind' P Case1 Case2 Case3 Case4 Case5 n)
  | Leaf v => Case3 v
  | 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.

Lemma h_injective_contr : forall n s n' s',
   h n s = h n' s' -> (n,s) = (n',s').
Proof.
Admitted.

Lemma merge_injective_contr : forall a b a' b',
    (a ^^ b) = (a' ^^ b') -> (a,b) = (a',b').
Proof.
Admitted.

Theorem hash_CR_contr : forall n1 n2,
    hash n1 = hash n2 -> n1 = n2.
Proof.
  induction n1 using node_ind'.
  - (* n1 = Bud None *)
    destruct n2 as [[n' |] | | |]; simpl; intro hash_eq.
    + now destruct (h_not_eq_zero 2 (hash n')).
    + reflexivity.
    + now destruct (h_not_eq_zero 0 (hash_of_value v )).
    + now destruct (h_not_eq_zero 1 (hash n2_1 ^^ hash n2_2)).
    + (* Extenderのsegがnon emptyであることと、non emptyがあるmergeがnon empty (公理) を使って証明 *)
      admit.
  - (* n1 = Bud (Some n) *)
    destruct n2 as [[n' |] | | |]; simpl; intro hash_eq.
    + do 2 f_equal. apply IHn1.
      apply h_injective_contr in hash_eq. now injection hash_eq.
    + edestruct h_not_eq_zero. exact hash_eq.
    + now edestruct h_injective; [|exact hash_eq].
    + now edestruct h_injective; [|exact hash_eq].
    + (* n2 = Extender s n2 の場合
      h 2 (hash n1) <> (hash n2 ^^ s) であることが必要
       *)
      admit.
  - (* n1 = Leaf v *)
    destruct n2 as [[n' |] | | |]; simpl; intro hash_eq.
    + now edestruct h_injective; [|exact hash_eq].
    + edestruct h_not_eq_zero. exact hash_eq.
    + apply h_injective_contr in hash_eq. injection hash_eq. intro eq.
      now rewrite (hash_of_value_injective_contr _ _ eq).
    + now edestruct h_injective; [|exact hash_eq].
    + (* n2 = Extender s n2 の場合
         h 0 (hash_of_value v) <> (hash n2 ^^ s) となることが必要
       *)
      admit.
  - (* n1 = Internal n1 n2 *)
    destruct n2 as [[n' |] | | |]; simpl; intro hash_eq.
    + now edestruct h_injective; [|exact hash_eq].
    + edestruct h_not_eq_zero. exact hash_eq.
    + now edestruct h_injective; [|exact hash_eq].
    + (* n2も Internalのとき *)
      injection (h_injective_contr _ _ _ _ hash_eq). intro merge_eq.
      injection (merge_injective_contr _ _ _ _  merge_eq). intros eq1 eq2.
      now rewrite IHn1_1 with (n2 := n2_1), IHn1_2 with (n2 := n2_2).
    + (* n2 = Extender s n2 の場合
         h 1 (hash n1_1 ^^ hash n1_2) <> (hash n2 ^^ s) であることが必要
       *)
      admit.
  - (* n1 = Extender seg n *)
    destruct n2 as [[n' |] | | |]; simpl; intro hash_eq.
    +
    (*  (hash n1 ^^ s) <> h 2 (hash n') *)
      admit.
    + (* Extのsegはnon_emptyを使う *)
      admit.
    + (*
        (hash n1 ^^ s) <> h 0 (hash_of_value v) *)
      admit.
    + (* (hash n1 ^^ s) <> h 1 (hash n2_1 ^^ hash n2_2) *)
      admit.
    + injection (merge_injective_contr _ _ _ _ hash_eq). intros seg_eq hash_eq'.
      now rewrite seg_eq, (IHn1 _ hash_eq').
Admitted.

Theorem hash_CR : forall n1 n2,
    n1 <> n2 -> hash n1 <> hash n2.
Proof.
  intros n1 n2 neq hash_eq.
  exact (neq (hash_CR_contr _ _ hash_eq)).
Qed.

Premise.v

Parameter hash : Set.
Parameter zerohash : hash.

Definition segment : Set := hash.
Parameter zerosegment : segment.

(*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 :=
| Bud : option node -> node
| Leaf : value -> node
| Internal : node -> node -> node
| Extender : segment -> node -> node.

Parameter h : nat -> hash -> hash.
Axiom h_injective: forall n s n' s'
   (n,s) <> (n',s')  ->   h n s <> h n' s'.

Axiom h_not_eq_zero : forall n s,
   h n s <> zerohash.

Parameter merge : hash -> hash -> hash.

Infix "^^" := merge (at level 80).

Axiom merge_injective : forall a b a' b',
   (a,b) <> (a',b') -> (a ^^ b) <> (a' ^^ b').