(* CAP theorem *)

Require Import Lia.

Inductive Value : Type :=
  | V1   : Value
  | V0   : Value
  | None : Value.

Class NetworkModel := {
  (* Number of network parts *)
  (* All parts are initialized with V0 *)
  n : nat;
  
  (* write to part[i], read from part[j] and reset all parts to V0 *)
  wr : forall (i j : nat), 
              i < n -> 
              j < n -> 
              Value;
              
  is_consistent : Prop :=
    forall (i j : nat) (Hi : i < n) (Hj : j < n),
    wr i j Hi Hj = V1 \/ wr i j Hi Hj = None;
    
  is_available : Prop :=
    forall (i j : nat) (Hi : i < n) (Hj : j < n),
    wr i j Hi Hj = V0 \/ wr i j Hi Hj = V1;

  is_partitioned : Prop :=
    n > 1;

  (* Behavior of two partitions *)
  wr_diff_parts : 
    forall (i j : nat) (Hi : i < n) (Hj : j < n),
    i <> j -> 
    (wr i j Hi Hj <> V1 \/ wr j i Hj Hi <> V1)
}.

(* If the NetworkModel is partitioned and consistent then there is at least one None response from wr *)
Lemma pc_exists_None :
  forall (model : NetworkModel),
  model.(is_partitioned)  /\ model.(is_consistent)  ->
  exists (i j : nat) (Hi : i < model.(n)) (Hj : j < model.(n)),
  model.(wr) i j Hi Hj = None.
Proof.
  intros model [H_partitioned H_c01].
  assert (H_c10 := H_c01).

  (* Since the model is partitioned, n > 1 *)
  unfold is_partitioned in H_partitioned.
  assert (Hn : model.(n) >= 2) by lia.

  (* Choose two distinct indices i and j *)
  assert (H0 : 0 < model.(n)) by lia.
  assert (H1 : 1 < model.(n)) by lia.
  assert (H01_neq : 0 <> 1) by lia.
  assert (H10_neq : 1 <> 0) by lia.  

  (* Apply the wr_diff_parts *)
  pose proof (model.(wr_diff_parts)  0 1 H0 H1 H01_neq) as H_p.
  unfold is_consistent in H_c10.
  unfold is_consistent in H_c01.
  specialize (H_c01 0 1 H0 H1).
  specialize (H_c10 1 0 H1 H0).
  
  destruct H_p as [H_p01 | H_p10].
- exists 0, 1, H0, H1.
  
  destruct H_c01 as [H_v1 | H_none].
+ (* Case: wr model 0 1 H0 H1 = V1 *)
  contradiction H_v1. 
+ (* Case: wr model 0 1 H0 H1 = None *)
  exact H_none.
  
- exists 1, 0, H1, H0.
  destruct H_c10 as [H_v1 | H_none].
  + (* Case: wr model 1 0 H1 H0 = V1 *)
  contradiction H_v1. 
  + (* Case: wr model 1 0 H1 H0 = None *)
  exact H_none. 
 
Qed.

Theorem cap :
  forall (model : NetworkModel),
  model.(is_partitioned)  ->
  ~ ( model.(is_consistent)  /\ model.(is_available) ).
Proof.
  intros model Hp Hca.
  
  destruct Hca as [Hc Ha].
  
  (* exists wr = None *)  
  pose proof (pc_exists_None model).
  assert (Hpc: model.(is_partitioned)  /\ model.(is_consistent) ).
  split.
  exact Hp.
  exact Hc.
  apply H in Hpc as HexistsNone.
  
  unfold is_available in Ha.
  destruct HexistsNone as [i [j [Hi [Hj Heq]]]].
  specialize (Ha i j Hi Hj).
  
  (* Ha says wr i j Hi Hj = V0 \/ wr i j Hi Hj = V1 *)
  (* Heq says wr i j Hi Hj = None *)
  (* None is neither V0 nor V1, contradiction *)
  rewrite Heq in Ha.
  destruct Ha as [HV0 | HV1].
  - discriminate HV0.
  - discriminate HV1.
Qed.

You can load it to the Coq scratchpad.