text:
Require Import Category.Lib.
Require Import Category.Theory.Category.
Require Import Category.Theory.Functor.
Require Import Category.Theory.Naturality.
Require Import Category.Functor.Bifunctor.
Require Import Category.Structure.Monoidal.

Generalizable All Variables.

Section MonoidalNaturality.

Context `{M : @Monoidal C}.

Program Definition Tensor_Left {F : C ⟶ C} {y : C} : C ⟶ C := {|
  fobj := fun x => (F x ⨂ y)%object;
  fmap := fun _ _ f => fmap[F] f ⨂[M] id
|}.
Next Obligation.
  proper; apply bimap_respects; rewrites; reflexivity.
Defined.
Next Obligation. normal; reflexivity. Qed.

#[export] Program Instance Tensor_Left_Map `{@Mapping C P} {y : C} :
  @Mapping C (fun x => P x ⨂ y)%object := {
  map := fun _ _ f => map f ⨂ id;
}.

#[export] Program Instance Tensor_Right {F : C ⟶ C} {x : C} : C ⟶ C := {
  fobj := fun y => (x ⨂ F y)%object;
  fmap := fun _ _ f => id ⨂[M] fmap[F] f
}.
Next Obligation.
  proper; apply bimap_respects;
  rewrites; reflexivity.
Qed.
Next Obligation. normal; reflexivity. Qed.

#[export] Program Instance Tensor_Right_Map `{@Mapping C P} {x : C} :
  @Mapping C (fun y => x ⨂ P y)%object := {
  map := fun _ _ f => id ⨂ map f;
}.

Program Definition Tensor_Both `{F : C ⟶ C} : C ⟶ C := {|
  fobj := fun x => (F x ⨂ F x)%object;
  fmap := fun _ _ f => fmap[F] f ⨂[M] fmap[F] f
|}.
Next Obligation.
  proper; apply bimap_respects;
  rewrites; reflexivity.
Qed.
Next Obligation. normal; reflexivity. Qed.

#[export] Program Instance Tensor_Both_Map `{@Mapping C P} :
  @Mapping C (fun x => P x ⨂ P x)%object := {
  map := fun _ _ f => map f ⨂ map f;
}.

Theorem monoidal_naturality :
  natural (@unit_left _ M) *
  natural (@unit_right _ M) *
  natural (@tensor_assoc _ M).
Proof. prove_naturality M normal. Qed.

End MonoidalNaturality.

author: jwiegley

repo: category-theory


text:
From CoqAlgs Require Export Base.
From CoqAlgs Require Export Sorting.Sort.
From CoqAlgs Require Export ListLemmas.
From CoqAlgs Require Import BST.
From CoqAlgs Require Export SplayTree.

Set Implicit Arguments.

Fixpoint fromList {A : Type} (p : A -> A -> bool) (l : list A) : SplayTree A :=
match l with
    | [] => empty
    | h :: t => insert p h (fromList p t)
end.

Definition splaySort {A : Type} (p : A -> A -> bool) (l : list A) : list A :=
  inorder (fromList p l).

Lemma isBST_fromList :
  forall (A : Type) (p : A -> A -> comparison) (l : list A),
    isBST p (fromList p l).
Proof.
  induction l as [| h t]; cbn.
    constructor.
    apply isBST_insert. assumption.
Qed.

Theorem Sorted_splaySort :
  forall {A : Ord} (l : list A),
    Sorted cmp (splaySort cmp l).
Proof.
  intros. unfold splaySort. apply Sorted_inorder, isBST_fromList.
Qed.

Lemma Permutation_splay :
  forall (A : Ord) (p : A -> A -> bool) (pivot : A) (h h1 h2 : SplayTree A),
    splay p pivot h = (h1, h2) ->
      Permutation (inorder h) (inorder h1 ++ inorder h2).
Proof.
  intros A p pivot h.
  functional induction @splay A p pivot h; cbn in *; inv 1.
    cbn. rewrite app_nil_r. reflexivity.
    cbn. rewrite <- !app_assoc. cbn. apply Permutation_app.
      reflexivity.
      constructor. apply Permutation_app.
        reflexivity.
        constructor. apply IHp0. assumption.
    cbn. rewrite <- !app_assoc. cbn. apply Permutation_app.
      reflexivity.
      constructor. rewrite (IHp0 _ _ e3). rewrite <- !app_assoc. reflexivity.
    cbn. rewrite (IHp0 _ _ e3). rewrite <- !app_assoc. cbn.
      rewrite <- app_assoc. reflexivity.
    rewrite (IHp0 _ _ e3). cbn. rewrite <- !app_assoc. reflexivity.
Qed.

Lemma Permutation_inorder_insert :
  forall (A : Ord) (p : A -> A -> bool) (x : A) (t : BTree A),
    Permutation (inorder (insert p x t)) (x :: inorder t).
Proof.
  induction t as [| v l r]; cbn.
    reflexivity.
    unfold insert. destruct (splay p x (node v l t1)) eqn: Heq.
      cbn. rewrite Permutation_app_comm. cbn. constructor.
        rewrite (@Permutation_splay _ _ _ _ _ _ Heq).
          apply Permutation_app_comm.
Qed.

Theorem Permutation_splaySort :
  forall (A : Ord) (p : A -> A -> bool) (l : list A),
    Permutation (splaySort p l) l.
Proof.
  intros. unfold splaySort.
  induction l as [| h t]; cbn.
    reflexivity.
    rewrite Permutation_inorder_insert. constructor. assumption.
Qed.

#[export]
Instance Sort_splaySort (A : Ord) : Sort cmp :=
{
    sort := splaySort trich_leb;
    Sorted_sort := Sorted_splaySort;
    Permutation_sort := Permutation_splaySort A cmp;
}.

(* Another way to prove permutation properties *)

Lemma countBT_splay :
  forall (A : Type) (cmp : A -> A -> bool) (p : A -> bool) (pivot : A) (h h1 h2 : SplayTree A),
    splay cmp pivot h = (h1, h2) ->
      countBT p h = countBT p h1 + countBT p h2.
Proof.
  intros until h. revert p.
  functional induction splay cmp pivot h;
  inv 1; cbn; erewrite IHp; eauto;
  destruct (p x), (p y); cbn; unfold id; lia.
Qed.

Lemma countBT_insert :
  forall (A : Type) (cmp : A -> A -> bool) (p : A -> bool) (x : A) (h : SplayTree A),
    countBT p (insert cmp x h) =
    (if p x then 1 else 0) + countBT p h.
Proof.
  intros. unfold insert.
  destruct (splay cmp x h) eqn: Heq.
  apply (countBT_splay cmp p) in Heq.
  rewrite Heq. cbn. destruct (p x); reflexivity.
Qed.

Lemma countBT_merge :
  forall (A : Type) (cmp : A -> A -> bool) (p : A -> bool) (h1 h2 : SplayTree A),
    countBT p (merge cmp h1 h2) = countBT p h1 + countBT p h2.
Proof.
  intros until h2.
  functional induction (merge cmp h1 h2); cbn.
    reflexivity.
    apply (countBT_splay cmp p) in e0.
      destruct (p v); unfold id; lia.
Qed.

Lemma countBT_fromList :
  forall (A : Type) (cmp : A -> A -> bool) (p : A -> bool) (l : list A),
    countBT p (fromList cmp l) = Perm.count p l.
Proof.
  induction l as [| h t]; cbn.
    reflexivity.
    rewrite countBT_insert. rewrite IHt.
      destruct (p h); reflexivity.
Qed.

Theorem perm_splaySort :
  forall (A : Type) (cmp : A -> A -> bool) (l : list A),
    perm l (splaySort cmp l).
Proof.
  unfold splaySort, perm. intros.
  rewrite count_toList. rewrite countBT_fromList. reflexivity.
Qed.

author: wkolowski

repo: coq-algs

save_path: github-repos/coq/wkolowski-coq-algs


text:
Require Import Basics Types HFiber Truncations.Core Truncations.SeparatedTrunc Pointed
  Modalities.ReflectiveSubuniverse.

Local Open Scope pointed_scope.

(** * [O]-connected covers *)

(** Given a reflective subuniverse [O], for any type [X] and [x : O X], the [O]-connected cover of [X] at [x] is the fibre of [to O X] at [x]. *)
Definition O_cover@{u} `{O : ReflectiveSubuniverse@{u}}
  (X : Type@{u}) (x : O X) : Type@{u}
  := hfiber (to O _) x.

(** The "[O]-connected" cover is in fact [O]-connected when [O] is a modality, using [isconnected_hfiber_conn_map]. Since Coq can infer this using typeclasses, we don't restate it here. *)

(** Characterization of paths in [O_cover] is given by [equiv_path_hfiber]. *)

(* If [x] is an actual point of [X], then the connected cover is pointed. *)
Definition O_pcover@{u} (O : ReflectiveSubuniverse@{u})
  (X : Type@{u}) (x : X) : pType@{u}
  := pfiber@{u u u} (pto O [X,x]).

(** Covers commute with products *)
Definition O_pcover_prod `{O : ReflectiveSubuniverse} {X Y : pType@{u}}
  : O_pcover O (X * Y) pt <~>* [(O_pcover O X pt) * (O_pcover O Y pt), _].
Proof.
  srapply Build_pEquiv'.
  { refine (_ oE equiv_functor_sigma_id _).
    2: intro; nrapply equiv_path_O_prod.
    nrapply equiv_sigma_prod_prod. }
  nrapply path_prod; cbn.
  all: snrapply path_sigma'.
  1,3: exact idpath.
  all: cbn.
  all: by rewrite concat_p1, concat_Vp.
Defined.

(** ** Functoriality of [O_cover] *)

(** Given [X] and [x : O X], any map [f : X -> Y] out of [X] induces a map [O_cover X x -> O_cover Y (O_functor O f x)]. *)
Definition functor_O_cover@{u v} `{O : ReflectiveSubuniverse} {X Y : Type@{u}}
  (f : X -> Y) (x : O X) : O_cover@{u} X x -> O_cover@{u} Y (O_functor O f x)
  := functor_hfiber (f:=to O _) (g:=to O _)
       (h:=f) (k:=O_functor O f) (to_O_natural O f) x.

Definition equiv_functor_O_cover `{O : ReflectiveSubuniverse}
  {X Y : Type} (f : X -> Y) `{IsEquiv _ _ f} (x : O X)
  : O_cover X x <~> O_cover Y (O_functor O f x)
  := Build_Equiv _ _ (functor_O_cover f x) _.

(** *** Pointed functoriality *)

Definition pfunctor_O_pcover `{O : ReflectiveSubuniverse} {X Y : pType}
  (f : X ->* Y) : O_pcover O X pt ->* O_pcover O Y pt
  := functor_pfiber (pto_O_natural O f).

Definition pequiv_pfunctor_O_pcover `{O : ReflectiveSubuniverse} {X Y : pType}
  (f : X ->* Y) `{IsEquiv _ _ f} : O_pcover O X pt <~>* O_pcover O Y pt
  := Build_pEquiv _ _ (pfunctor_O_pcover f) _.

(** In the case of truncations, [ptr_natural] gives a better proof of pointedness. *)
Definition pfunctor_pTr_pcover `{n : trunc_index} {X Y : pType}
  (f : X ->* Y) : O_pcover (Tr n) X pt ->* O_pcover (Tr n) Y pt
  := functor_pfiber (ptr_natural n f).

Definition pequiv_pfunctor_pTr_pcover `{n : trunc_index}
  {X Y : pType} (f : X ->* Y) `{IsEquiv _ _ f}
  : O_pcover (Tr n) X pt <~>* O_pcover (Tr n) Y pt
  := Build_pEquiv _ _ (pfunctor_pTr_pcover f) _.

(** * Components *)

(** Path components are given by specializing to [O] being set-truncation. *)
Definition comp := O_cover (O:=Tr 0).
Definition pcomp := O_pcover (Tr 0).

Definition pfunctor_pcomp {X Y : pType} := @pfunctor_pTr_pcover (-1) X Y.
Definition pequiv_pfunctor_pcomp {X Y : pType}
  := @pequiv_pfunctor_pTr_pcover (-1) X Y.

(** If a property holds at a given point, then it holds for the whole component. This yields equivalences like the following: *)
Definition equiv_comp_property `{Univalence} {X : Type} (x : X)
  (P : X -> Type) `{forall x, IsHProp (P x)} (Px : P x)
  : comp (sig P) (tr (x; Px)) <~> comp X (tr x).
Proof.
  unfold comp, O_cover, hfiber. simpl.
  refine (_ oE (equiv_sigma_assoc _ _)^-1).
  apply equiv_functor_sigma_id; intro y.
  apply equiv_iff_hprop.
  - intros [py q].
    exact (ap (Trunc_functor _ pr1) q).
  - refine (equiv_ind (equiv_path_Tr _ _) _ _).
    apply Trunc_rec; intros p; induction p.
    exact (Px; idpath).
Defined.

(** For example, we may take components of equivalences among underlying maps. *)
Definition equiv_comp_equiv_map `{Univalence} {A B : Type} (e : A <~> B)
  : comp (A <~> B) (tr e) <~> comp (A -> B) (tr (equiv_fun e)).
Proof.
  refine (_ oE equiv_functor_O_cover (issig_equiv _ _)^-1 _); cbn.
  rapply equiv_comp_property.
Defined.

author: HoTT

repo: Coq-HoTT

save_path: github-repos/coq/HoTT-Coq-HoTT


text:
Require Import Coq.Lists.List.

Require Import Category.Lib.
Require Import Category.Instance.Lambda.Exp.

From Equations Require Import Equations.
Set Equations With UIP.

Generalizable All Variables.

Section Value.

Import ListNotations.

Open Scope Ty_scope.

(* [ValueP] is an inductive proposition that indicates whether an expression
   represents a value, i.e., that it does reduce any further. *)
Inductive ValueP Γ : ∀ {τ}, Exp Γ τ → Type :=
  | UnitP : ValueP EUnit
  | PairP {τ1 τ2} {x : Exp Γ τ1} {y : Exp Γ τ2} :
    ValueP x → ValueP y → ValueP (Pair x y)
  | LambdaP {dom cod} (e : Exp (dom :: Γ) cod) : ValueP (LAM e).

Derive Signature for ValueP.

#[local] Hint Constructors ValueP : core.

Fixpoint ValueP_irrelevance {Γ τ} (v : Exp Γ τ) (H1 H2 : ValueP _ v) :
  H1 = H2.
Proof.
  dependent elimination H1;
  dependent elimination H2.
  - reflexivity.
  - f_equal;
    now apply ValueP_irrelevance.
  - f_equal;
    now apply ValueP_irrelevance.
Qed.

Lemma ValueP_dec {Γ τ} (e : Exp Γ τ) :
  ValueP Γ e ∨ ¬ ValueP Γ e.
Proof.
  induction e; try solve [now left|now right].
  destruct IHe1, IHe2.
  - left.
    now constructor.
  - right.
    intro.
    dependent elimination H.
    contradiction.
  - right.
    intro.
    dependent elimination H.
    contradiction.
  - right.
    intro.
    dependent elimination H.
    contradiction.
Qed.

End Value.

Arguments ValueP {Γ τ} _.
Arguments UnitP {Γ}.
Arguments PairP {Γ τ1 τ2 x y} _ _.
Arguments LambdaP {Γ dom cod} _.


text:
From VLSM.Lib Require Import Itauto.
From stdpp Require Import prelude finite.
From Coq Require Import FunctionalExtensionality.
From VLSM.Lib Require Import Preamble StdppListFinSet.
From VLSM.Core Require Import VLSM MessageDependencies ProjectionTraces VLSMProjections.
From VLSM.Core Require Import Composition SubProjectionTraces ByzantineTraces.
From VLSM.Core Require Import Validator Equivocation EquivocationProjections.
From VLSM.Core Require Import Equivocation.NoEquivocation Equivocation.FixedSetEquivocation.

(** * VLSM Compositions with a fixed set of byzantine nodes

  In this module we study a composition in which a fixed subset of nodes are
  replaced by byzantine nodes, i.e., nodes which can send arbitrary
  [channel_authenticated_message]s at any time, while the rest are protocol
  abiding (non-equivocating) nodes.

  We will show that, if the non-byzantine nodes are validators for the
  composition with that specific fixed-set of nodes as equivocators, then the
  projections of traces to the non-byzantine nodes are precisely the projections
  of traces of the composition with that specific fixed-set of nodes as
  equivocators to the non-equivocating nodes.

  That is, non-byzantine validator nodes do not distinguish between byzantine
  nodes and equivocating ones.  Therefore, when analyzing the security of a
  protocol it suffices to consider equivocating nodes.
*)

Section sec_emit_any_signed_message_vlsm.

(** ** A machine which can emit any valid message for a given node

  This VLSM is similar to the [emit_any_message_vlsm] with the exception of the
  validity predicate which requires that the sender of the emitted message
  corresponds to the given node.
*)

Context
  {message : Type}
  {index : Type}
  {validator : Type}
  (A : validator -> index)
  (sender : message -> option validator)
  (node_idx : index)
  .

(** The [valid]ity predicate allows sending only signed messages *)
Definition signed_messages_valid
  (l : @label message all_messages_type)
  (som : @state message all_messages_type * option message)
  : Prop :=
  channel_authenticated_message A sender node_idx l.

Definition emit_any_signed_message_vlsm_machine
  : VLSMMachine all_messages_type
  :=
  {| initial_state_prop := fun s => True
   ; initial_message_prop := fun m => False
   ; s0 := all_messages_state_inh
   ; transition := all_messages_transition
   ; valid := signed_messages_valid
  |}.

Definition emit_any_signed_message_vlsm
    := mk_vlsm emit_any_signed_message_vlsm_machine.

End sec_emit_any_signed_message_vlsm.

Section sec_fixed_byzantine_traces.

Context
  {message : Type}
  `{FinSet index Ci}
  `{@finite.Finite index _}
  (IM : index -> VLSM message)
  `{forall i : index, HasBeenSentCapability (IM i)}
  (byzantine : Ci)
  {validator : Type}
  (A : validator -> index)
  (sender : message -> option validator)
  (no_initial_messages_in_IM : no_initial_messages_in_IM_prop IM)
  (can_emit_signed : channel_authentication_prop IM A sender)
  (Hsender_safety : sender_safety_alt_prop IM A sender :=
    channel_authentication_sender_safety IM A sender can_emit_signed)
  .

(**
  Given a collection of nodes indexed by an <<index>>, we define the
  associated fixed byzantine collection of nodes by replacing the nodes
  corresponding to the indices in a given <<byzantine>> with byzantine nodes,
  i.e., nodes which can emit any (signed) message.
*)
Definition fixed_byzantine_IM : index -> VLSM message :=
  update_IM IM byzantine (fun i => emit_any_signed_message_vlsm A sender (` i)).

Lemma fixed_byzantine_IM_no_initial_messages
  : forall i m, ~ vinitial_message_prop (fixed_byzantine_IM i) m.
Proof.
  unfold fixed_byzantine_IM, update_IM. simpl.
  intros i m Hm.
  by case_decide; [| destruct (no_initial_messages_in_IM i m)].
Qed.

Lemma fixed_byzantine_IM_preserves_channel_authentication
: channel_authentication_prop fixed_byzantine_IM A sender.
Proof.
  unfold fixed_byzantine_IM, update_IM. simpl.
  intros i m Hm.
  case_decide; [| by apply can_emit_signed].
  destruct Hm as [(s0, om) [l [s1 [[_ [_ Hv]] Ht]]]].
  cbn in Hv, Ht.
  unfold signed_messages_valid, channel_authenticated_message in Hv.
  by inversion Ht; subst.
Qed.

Definition fixed_byzantine_IM_sender_safety
  : sender_safety_alt_prop fixed_byzantine_IM A sender :=
  channel_authentication_sender_safety fixed_byzantine_IM A sender
    fixed_byzantine_IM_preserves_channel_authentication.

Definition message_as_byzantine_label
  (m : message)
  (i : index)
  (Hi : i ∈ byzantine)
  : composite_label fixed_byzantine_IM.
Proof.
  exists i.
  unfold fixed_byzantine_IM, update_IM.
  simpl.
  by rewrite decide_True; [| apply elem_of_elements, Hi].
Defined.

Context
  (non_byzantine : Ci := difference (list_to_set (enum index)) byzantine)
  .

(** Constraint requiring only that the non-byzantine nodes are not equivocating. *)
Definition non_byzantine_not_equivocating_constraint
  : composite_label fixed_byzantine_IM ->
    composite_state fixed_byzantine_IM * option message -> Prop :=
      sub_IM_not_equivocating_constraint fixed_byzantine_IM (elements non_byzantine) A sender.

(** *** First definition of the fixed byzantine trace property

  Fixed byzantine traces are projections to the subset of protocol-following nodes
  of traces which are valid for the composition in which a fixed set of nodes
  were replaced by byzantine nodes and the rest are protocol-following
  (i.e., they are not equivocating).
*)
Definition fixed_byzantine_trace_prop
  (is : composite_state (sub_IM fixed_byzantine_IM (elements non_byzantine)))
  (tr : list (composite_transition_item (sub_IM fixed_byzantine_IM (elements non_byzantine))))
  : Prop :=
  exists bis btr,
    finite_valid_trace
      (composite_vlsm fixed_byzantine_IM non_byzantine_not_equivocating_constraint) bis btr /\
    composite_state_sub_projection fixed_byzantine_IM (elements non_byzantine) bis = is /\
    finite_trace_sub_projection fixed_byzantine_IM (elements non_byzantine) btr = tr.

(** ** Byzantine traces characterization as projections *)

Section sec_fixed_byzantine_traces_as_projections.

Definition fixed_non_byzantine_projection : VLSM message :=
  pre_induced_sub_projection fixed_byzantine_IM (elements non_byzantine)
    non_byzantine_not_equivocating_constraint.

Lemma fixed_non_byzantine_projection_initial_state_preservation
  : forall s, vinitial_state_prop fixed_non_byzantine_projection s <->
    composite_initial_state_prop (sub_IM fixed_byzantine_IM (elements non_byzantine)) s.
Proof.
  split.
  - intros Hs sub_i.
    destruct Hs as [sX [HeqsX Hinitial]].
    subst.
    by apply Hinitial.
  - intros Hs.
    exists (lift_sub_state fixed_byzantine_IM (elements non_byzantine) s).
    split.
    + by apply composite_state_sub_projection_lift_to.
    + by apply (lift_sub_state_initial fixed_byzantine_IM (elements non_byzantine)).
Qed.

Lemma fixed_non_byzantine_projection_incl_preloaded :
  VLSM_incl
    fixed_non_byzantine_projection
    (pre_loaded_with_all_messages_vlsm
      (free_composite_vlsm (sub_IM fixed_byzantine_IM (elements non_byzantine)))).
Proof.
  apply basic_VLSM_strong_incl.
  - by intros s Hincl; apply fixed_non_byzantine_projection_initial_state_preservation.
  - by intros.
  - by split; [eapply induced_sub_projection_valid_preservation |].
  - intros l s om s' om'; cbn.
    (* an ugly trick to get the forward direction from an iff (<->) lemma *)
    by eapply proj1; rapply @induced_sub_projection_transition_preservation.
Qed.

(**
  The induced projection from the composition of [fixed_byzantine_IM] under
  the [non_byzantine_not_equivocating_constraint] to the non-byzantine nodes has
  the [projection_friendly_prop]erty.
*)
Lemma fixed_non_byzantine_projection_friendliness
  : projection_friendly_prop
      (induced_sub_projection_is_projection fixed_byzantine_IM (elements non_byzantine)
        non_byzantine_not_equivocating_constraint).
Proof.
  apply induced_sub_projection_friendliness.
  apply induced_sub_projection_lift.
  intros s1 s2 Heq l om.
  destruct om as [m |]; [| by itauto].
  cbn.
  destruct (sender m) as [v |]; [| by itauto].
  simpl.
  case_decide as HAv; [| by itauto].
  replace (s2 (A v)) with (s1 (A v)); [by itauto |].
  exact (equal_f_dep Heq (dexist (A v) HAv)).
Qed.

(**
  Characterization result for the first definition:
  the [fixed_byzantine_trace_prop]erty is equivalent to the
  [finite_valid_trace_prop]erty of the [pre_induced_sub_projection] of the
  the composition in which a fixed set of nodes were replaced by byzantine nodes
  and the rest are protocol-following to the set of protocol-following nodes.
*)
Lemma fixed_byzantine_trace_char1 is tr
  : fixed_byzantine_trace_prop is tr <->
    finite_valid_trace fixed_non_byzantine_projection is tr.
Proof.
  apply and_comm.
  apply (projection_friendly_trace_char (induced_sub_projection_is_projection _ _ _)).
  by apply fixed_non_byzantine_projection_friendliness.
Qed.

End sec_fixed_byzantine_traces_as_projections.

(** ** Fixed Byzantine traces as traces pre-loaded with signed messages

  In this section we'll be showing that byzantine traces correspond to traces of
  the composition of nodes in the [non_byzantine], preloaded with messages
  signed by the nodes in the <<byzantine>>.
*)

Section sec_fixed_byzantine_traces_as_pre_loaded.

Definition fixed_set_signed_message (m : message) : Prop :=
  non_sub_index_authenticated_message (elements non_byzantine) A sender m /\
  (exists i, i ∈ non_byzantine /\
    exists l s, input_valid (pre_loaded_with_all_messages_vlsm (IM i)) l (s, Some m)).

(**
  Given that we're only looking at the composition of nodes in the
  [non_byzantine], we can define their subset as either a subset of the
  [fixed_byzantine_IM] or of the original <<IM>>.

  As it turns out, the first definition is easier to prove equivalent to the
  induced [fixed_non_byzantine_projection], while the second is easier to work
  with in general because it makes no reference to byzantine nodes.

  Therefore we'll first be defining them both below and show that they are
  equivalent to each-other using the generic Lemma [same_IM_embedding].
*)

Definition pre_loaded_fixed_non_byzantine_vlsm' : VLSM message :=
  composite_no_equivocation_vlsm_with_pre_loaded (sub_IM fixed_byzantine_IM (elements non_byzantine))
    (free_constraint _) fixed_set_signed_message.

Definition pre_loaded_fixed_non_byzantine_vlsm : VLSM message :=
  composite_no_equivocation_vlsm_with_pre_loaded (sub_IM IM (elements non_byzantine)) (free_constraint _)
    fixed_set_signed_message.

Lemma non_byzantine_nodes_same
  : forall sub_i, sub_IM fixed_byzantine_IM (elements non_byzantine) sub_i = sub_IM IM (elements non_byzantine) sub_i.
Proof.
  intro sub_i.
  destruct_dec_sig sub_i i Hi Heqsub_i.
  subst.
  unfold sub_IM, fixed_byzantine_IM, update_IM.
  simpl.
  apply elem_of_elements, set_diff_elim2 in Hi.
  by rewrite decide_False; [| rewrite elem_of_elements].
Qed.

Lemma non_byzantine_nodes_same_sym
  : forall sub_i, sub_IM IM (elements non_byzantine) sub_i = sub_IM fixed_byzantine_IM (elements non_byzantine) sub_i.
Proof.
  by intro; symmetry; apply non_byzantine_nodes_same.
Qed.

Lemma pre_loaded_fixed_non_byzantine_VLSM_embedding
  : VLSM_embedding
    pre_loaded_fixed_non_byzantine_vlsm'
    pre_loaded_fixed_non_byzantine_vlsm
    (same_IM_label_rew non_byzantine_nodes_same)
    (same_IM_state_rew non_byzantine_nodes_same).
Proof.
  apply same_IM_embedding.
  intros s1 Hs1 l1 om [Hom _].
  split; [| done].
  destruct om as [m |]; [| done].
  destruct Hom as [Hsent | Hseeded]; [| by right].
  by left; eapply same_IM_composite_has_been_sent_preservation.
Qed.

Lemma pre_loaded_fixed_non_byzantine_VLSM_embedding'
  : VLSM_embedding
    pre_loaded_fixed_non_byzantine_vlsm
    pre_loaded_fixed_non_byzantine_vlsm'
    (same_IM_label_rew non_byzantine_nodes_same_sym)
    (same_IM_state_rew non_byzantine_nodes_same_sym).
Proof.
  apply same_IM_embedding.
  intros s1 Hs1 l1 om [Hom _].
  split; [| done].
  destruct om as [m |]; [| done].
  destruct Hom as [Hsent | Hseeded]; [| by right].
  by left; eapply same_IM_composite_has_been_sent_preservation.
Qed.

(**
  We next show that the [fixed_non_byzantine_projection] and
  [pre_loaded_fixed_non_byzantine_vlsm'] are [VLSM_eq]ual.

  The validity of [fixed_non_byzantine_projection] subsumes
  the constraint of [pre_loaded_fixed_non_byzantine_vlsm'].
*)
Lemma fixed_non_byzantine_projection_valid_no_equivocations
  : forall l s om, vvalid fixed_non_byzantine_projection l (s, om) ->
    composite_no_equivocations_except_from
      (sub_IM fixed_byzantine_IM (elements non_byzantine))
      fixed_set_signed_message
      l (s, om).
Proof.
  intros l s om Hv.
  apply
    (sub_IM_no_equivocation_preservation fixed_byzantine_IM (elements non_byzantine)
      A sender fixed_byzantine_IM_sender_safety
      fixed_byzantine_IM_no_initial_messages fixed_byzantine_IM_preserves_channel_authentication)
    in Hv as Hnoequiv.
  destruct om as [m |]; [| done].
  destruct Hnoequiv as [Hsent | Hseeded]; [by left |].
  right.
  split; [done |].
  apply induced_sub_projection_valid_projection in Hv
    as [i [Hi [li [si Hv]]]].
  exists i.
  split; [by apply elem_of_elements in Hi |].
  revert li si Hv.
  unfold fixed_byzantine_IM, update_IM. simpl.
  apply elem_of_elements, set_diff_elim2 in Hi.
  by rewrite decide_False; [intros; exists li, si | rewrite elem_of_elements].
Qed.

Lemma fixed_non_byzantine_pre_loaded_incl
  : VLSM_incl fixed_non_byzantine_projection pre_loaded_fixed_non_byzantine_vlsm'.
Proof.
  apply basic_VLSM_incl.
  - by intro; intros; apply fixed_non_byzantine_projection_initial_state_preservation.
  - intros l s m (Hs & _ & Hv) HsY _.
    apply fixed_non_byzantine_projection_valid_no_equivocations
       in Hv as [Hsent | Hseeded].
    + simpl in Hsent, HsY.
      by eapply preloaded_composite_sent_valid.
    + by apply initial_message_is_valid; right.
  - intros l s om (_ & _ & Hv) _ _; split.
    + by eapply induced_sub_projection_valid_preservation.
    + split; [| done].
      by apply fixed_non_byzantine_projection_valid_no_equivocations.
  - intros l s om s' om' [_ Ht]; cbn.
    by apply induced_sub_projection_transition_preservation.
Qed.

Lemma pre_loaded_fixed_non_byzantine_vlsm_lift_valid
  : weak_embedding_valid_preservation pre_loaded_fixed_non_byzantine_vlsm'
    (composite_vlsm fixed_byzantine_IM
       non_byzantine_not_equivocating_constraint)
    (lift_sub_label fixed_byzantine_IM (elements non_byzantine))
    (lift_sub_state fixed_byzantine_IM (elements non_byzantine)).
Proof.
  intros (sub_i, li) s om (HsX & HomX & Hv & Hc & _) HsY HomY.
  destruct_dec_sig sub_i i Hi Heqsub_i; subst.
  split; [by apply lift_sub_valid |].
  clear -Hsender_safety Hc HsX.
  cbn; destruct om as [m |]; [| done].
  destruct (sender m) as [v |] eqn: Hsender; [| done]; cbn.
  case_decide as HAv; [| done].
  cbn in Hc; destruct Hc as [Hsent | Hseeded].
  - unfold lift_sub_state.
    rewrite (lift_sub_state_to_eq _ _ _ _ _ HAv).
    apply (sub_IM_has_been_sent_iff_by_sender fixed_byzantine_IM (elements non_byzantine)
            A sender fixed_byzantine_IM_sender_safety)
    ; [| done | done].
    eapply (VLSM_incl_valid_state); [| done].
    by eapply composite_pre_loaded_vlsm_incl_pre_loaded_with_all_messages.
  - contradict HAv; clear -Hseeded Hsender.
    destruct Hseeded as [(i & Hi & Hm) _].
    unfold channel_authenticated_message in Hm.
    rewrite Hsender in Hm.
    by inversion Hm; subst.
Qed.

Lemma pre_loaded_fixed_non_byzantine_vlsm_lift_initial_message
  : weak_embedding_initial_message_preservation
    pre_loaded_fixed_non_byzantine_vlsm'
    (composite_vlsm fixed_byzantine_IM
       non_byzantine_not_equivocating_constraint)
    (lift_sub_state fixed_byzantine_IM (elements non_byzantine)).
Proof.
  intros l s m Hv HsY HmX.
  destruct HmX as [[sub_i [[im Him] Heqm]] | Hseeded].
  - exfalso. clear -no_initial_messages_in_IM Him.
    destruct_dec_sig sub_i i Hi Heqsub_i.
    subst.
    unfold sub_IM, fixed_byzantine_IM, update_IM in Him.
    simpl in Him.
    by case_decide; [| destruct (no_initial_messages_in_IM i im)].
  - destruct Hseeded as [[i [Hi Hsender]] Hvalid].
    pose (X := (composite_vlsm fixed_byzantine_IM non_byzantine_not_equivocating_constraint)).
    pose (s0 := proj1_sig (composite_s0 fixed_byzantine_IM)).
    assert (Hs0 : valid_state_message_prop X s0 None).
    { apply (valid_initial_state_message X); [| done].
      by destruct (composite_s0 fixed_byzantine_IM).
    }
    specialize (valid_generated_state_message X _ _ Hs0 _ _ Hs0) as Hgen.
    unfold non_byzantine in Hi.
    pose proof (Hdec := elem_of_dec_slow (H6 := H6)).
    rewrite elem_of_elements in Hi; setoid_rewrite set_diff_iff in Hi.
    apply not_and_r in Hi as [Hi | Hi];
      [by elim Hi; apply elem_of_list_to_set, elem_of_enum |].
    apply dec_stable in Hi.
    specialize (Hgen (message_as_byzantine_label m i Hi)).
    spec Hgen.
    { split; [| done].
      cbn. unfold fixed_byzantine_IM, update_IM. simpl.
      by rewrite @decide_True.
    }
    cbn in Hgen.
    destruct (vtransition _ _ _) as (si', _om) eqn: Ht.
    specialize (Hgen _ _ eq_refl).
    replace _om with (Some m) in Hgen; [by eexists |].
    clear -Ht.
    revert si' Ht.
    unfold fixed_byzantine_IM, update_IM.
    simpl.
    rewrite @decide_True by done.
    cbn. unfold all_messages_transition.
    by inversion 1; itauto.
Qed.

(**
  Since the [fixed_non_byzantine_projection] is an [induced_validator] of
  the composition of [fixed_byzantine_IM] with a
  [non_byzantine_not_equivocating_constraint], its initial_messages and validity
  are derived from valid messages and protocol validity of the larger
  composition; therefore, the following simple result becomes very important.
*)
Lemma pre_loaded_fixed_non_byzantine_vlsm_lift :
  VLSM_embedding
    pre_loaded_fixed_non_byzantine_vlsm'
    (composite_vlsm fixed_byzantine_IM non_byzantine_not_equivocating_constraint)
    (lift_sub_label fixed_byzantine_IM (elements non_byzantine))
    (lift_sub_state fixed_byzantine_IM (elements non_byzantine)).
Proof.
  apply basic_VLSM_embedding.
  - by intro; intros; apply pre_loaded_fixed_non_byzantine_vlsm_lift_valid.
  - by intro; intros * []; rapply lift_sub_transition.
  - by intro; intros; apply (lift_sub_state_initial fixed_byzantine_IM).
  - by intro; intros; apply (pre_loaded_fixed_non_byzantine_vlsm_lift_initial_message l s m).
Qed.

Lemma pre_loaded_fixed_non_byzantine_incl
  : VLSM_incl pre_loaded_fixed_non_byzantine_vlsm' fixed_non_byzantine_projection.
Proof.
  apply basic_VLSM_incl; cbn.
  - by intro; intros; apply fixed_non_byzantine_projection_initial_state_preservation.
  - by intros l s m Hv _ Him; apply initial_message_is_valid.
  - intros l s om Hv.
    exists (lift_sub_label fixed_byzantine_IM (elements non_byzantine) l).
    exists (lift_sub_state fixed_byzantine_IM (elements non_byzantine) s).
    split.
    + by apply composite_label_sub_projection_option_lift.
    + by apply composite_state_sub_projection_lift.
    + by apply (VLSM_embedding_input_valid pre_loaded_fixed_non_byzantine_vlsm_lift).
  - by intros l s om s' om' [_ Ht]; apply induced_sub_projection_transition_preservation.
Qed.

Lemma fixed_non_byzantine_pre_loaded_eq
  : VLSM_eq fixed_non_byzantine_projection pre_loaded_fixed_non_byzantine_vlsm'.
Proof.
  split.
  - by apply fixed_non_byzantine_pre_loaded_incl.
  - by apply pre_loaded_fixed_non_byzantine_incl.
Qed.

End sec_fixed_byzantine_traces_as_pre_loaded.

(** *** Second fixed byzantine trace definition

  Given the equivalence results from Lemmas [fixed_byzantine_trace_char1],
  [fixed_non_byzantine_pre_loaded_eq], and
  [pre_loaded_fixed_non_byzantine_VLSM_embedding],
  we introduce the following alternate definition to the
  [fixed_byzantine_trace_prop]erty, this time defined for (not necessarily valid)
  traces of the full composition, accepting any such trace as long as its
  projection to the non-byzantine nodes is indistinguishable from a projection
  of a valid trace of the composition of [fixed_byzantine_IM] under the
  [non_byzantine_not_equivocating_constraint].
*)
Definition fixed_byzantine_trace_alt_prop is tr : Prop :=
  finite_valid_trace pre_loaded_fixed_non_byzantine_vlsm
    (composite_state_sub_projection IM (elements non_byzantine) is)
    (finite_trace_sub_projection IM (elements non_byzantine) tr).

End sec_fixed_byzantine_traces.

(** ** Relation between Byzantine nodes and equivocators

  In this section we show that while equivocators can always appear as byzantine
  to the protocol-abiding nodes, the converse is also true if the protocol-
  abiding nodes satisfy the [projection_message_validator_prop]erty, which basically
  allows them to locally verify the authenticity of a received message.
*)

Section sec_fixed_non_equivocating_vs_byzantine.

Context
  {message : Type}
  `{FinSet index Ci}
  `{@finite.Finite index _}
  (IM : index -> VLSM message)
  `{forall i : index, HasBeenSentCapability (IM i)}
  `{forall i : index, HasBeenReceivedCapability (IM i)}
  (selection : Ci)
  {validator : Type}
  (A : validator -> index)
  (sender : message -> option validator)
  (selection_complement := difference (list_to_set (enum index)) selection)
  (PreNonByzantine : VLSM message := pre_loaded_fixed_non_byzantine_vlsm IM selection A sender)
  (Fixed : VLSM message := fixed_equivocation_vlsm_composition IM selection)
  (FixedNonEquivocating : VLSM message :=
    pre_induced_sub_projection IM (elements selection_complement) (fixed_equivocation_constraint IM selection))
  (no_initial_messages_in_IM : no_initial_messages_in_IM_prop IM)
  (can_emit_signed : channel_authentication_prop IM A sender)
  (Hsender_safety : sender_safety_alt_prop IM A sender :=
    channel_authentication_sender_safety IM A sender can_emit_signed)
  .

Lemma fixed_non_equivocating_incl_sub_non_equivocating
  : VLSM_incl FixedNonEquivocating
      (pre_induced_sub_projection IM (elements selection_complement)
        (sub_IM_not_equivocating_constraint IM
          (elements selection_complement) A sender)).
Proof.
  apply induced_sub_projection_constraint_subsumption_incl.
  intros l (s, om) Hv.
  apply (fixed_strong_equivocation_subsumption IM selection)
    in Hv as Hstrong_v.
  destruct Hv as (Hs & Hom & Hv & Hc).
  destruct om; [| done].
  cbn; destruct (sender m) as [v |] eqn: Hsender; [| done]; cbn.
  case_decide as HAv; [| done].
  unfold sub_IM; cbn.
  apply (VLSM_incl_valid_state (constraint_free_incl IM
    (fixed_equivocation_constraint IM selection))) in Hs.
  apply (VLSM_incl_valid_state (vlsm_incl_pre_loaded_with_all_messages_vlsm
    (free_composite_vlsm IM))) in Hs.
  assert (Hpre_si : forall i, valid_state_prop (pre_loaded_with_all_messages_vlsm (IM i)) (s i)).
  {
    intro i.
    revert Hs.
    apply valid_state_project_preloaded_to_preloaded.
  }
  apply elem_of_elements, set_diff_elim2 in HAv.
  destruct Hstrong_v as [(i & Hi & Hsent) | Hemitted].
  - apply valid_state_has_trace in Hs as (is & tr & Htr).
    by eapply has_been_sent_iff_by_sender; [| | | exists i].
  - by contradict HAv; apply elem_of_elements; eapply sub_can_emit_sender.
Qed.

Lemma fixed_non_equivocating_incl_fixed_non_byzantine
  : VLSM_incl FixedNonEquivocating PreNonByzantine.
Proof.
  apply basic_VLSM_incl.
  - intros s (sX & <- & Hinitial) sub_i.
    by apply Hinitial.
  - intro; intros.
    apply (VLSM_incl_input_valid fixed_non_equivocating_incl_sub_non_equivocating)
      in Hv as (Hs & _ & Hv).
    apply sub_IM_no_equivocation_preservation in Hv as Hnoeqv; [| done..].
    destruct Hnoeqv as [Hsent | Hseeded].
    + by eapply preloaded_composite_sent_valid.
    + apply initial_message_is_valid.
      unfold initial_message_prop.
      right; split; [done |].
      destruct (induced_sub_projection_valid_projection IM
        (elements selection_complement) _ _ _ _ Hv) as (i & Hi & Hiv).
      by apply elem_of_elements in Hi; eexists; split.
  - intros l s om Hv.
    apply (VLSM_incl_input_valid fixed_non_equivocating_incl_sub_non_equivocating)
       in Hv as (_ & _ & Hv).
    split.
    + by eapply induced_sub_projection_valid_preservation.
    + split; [| done].
      apply sub_IM_no_equivocation_preservation in Hv as Hnoequiv; [| done..].
      destruct om as [m |]; [| done].
      destruct Hnoequiv as [Hsent | Hseeded]; [by left | right].
      split; [done |].
      destruct (induced_sub_projection_valid_projection IM
        (elements selection_complement) _ _ _ _ Hv) as (i & Hi & Hiv).
      by apply elem_of_elements in Hi; eexists; split.
  - intros l s om s' om' [_ Ht].
    revert Ht.
    by apply @induced_sub_projection_transition_preservation.
Qed.

(**
  As a corollary to the above result, we can conclude that valid
  traces for the composition with <<Fixed>> equivocation have the
  [fixed_byzantine_trace_alt_prop]erty.
*)
Corollary fixed_equivocating_traces_are_byzantine is tr
  : finite_valid_trace Fixed is tr ->
    fixed_byzantine_trace_alt_prop IM selection A sender is tr.
Proof.
  intro Htr.
  apply (VLSM_incl_finite_valid_trace fixed_non_equivocating_incl_fixed_non_byzantine).
  specialize
    (induced_sub_projection_is_projection
      IM (elements selection_complement) (fixed_equivocation_constraint IM selection))
    as Hproj.
  by apply (VLSM_projection_finite_valid_trace Hproj).
Qed.

Section sec_validator_fixed_set_byzantine.

Context
  `{FinSet message Cm}
  (message_dependencies : message -> Cm)
  `{!Irreflexive (msg_dep_happens_before message_dependencies)}
  `{forall i, MessageDependencies (IM i) message_dependencies}
  (Hfull : forall i, message_dependencies_full_node_condition_prop (IM i) message_dependencies)
  .

Lemma fixed_non_byzantine_vlsm_lift_valid
  : weak_embedding_valid_preservation PreNonByzantine Fixed
    (lift_sub_label IM (elements selection_complement))
    (lift_sub_state IM (elements selection_complement)).
Proof.
  intros l s om Hv HsY HomY.
  split.
  - by apply lift_sub_valid, Hv.
  - destruct om as [m |]; [| done].
    apply proj2 in Hv as Hc.
    destruct Hc as [_ [_ [Hc _]]].
    destruct Hc as [Hsent | Hseeded].
    + left.
      apply composite_has_been_directly_observed_sent_received_iff.
      left.
      simpl in Hsent. clear -Hsent.
      destruct Hsent as [sub_i Hsenti].
      destruct_dec_sig sub_i i Hi Heqsub_i.
      subst.
      exists i.
      unfold lift_sub_state.
      by rewrite (lift_sub_state_to_eq _ _ _ _ _ Hi).
    + right.
      apply emitted_messages_are_valid_iff in HomY.
      destruct HomY as [[_v [[_im Him] Heqim]] | Hiom]
      ; [by elim (no_initial_messages_in_IM _v _im) |].
      apply (VLSM_incl_can_emit (vlsm_incl_pre_loaded_with_all_messages_vlsm Fixed))
        in Hiom.
      apply can_emit_composite_project in Hiom as [_v Hiom].
      destruct Hseeded as [[i [Hi Hsigned]] _].
      unfold channel_authenticated_message in Hsigned.
      destruct (sender m) as [v |] eqn: Hsender; simpl in Hsigned; [| by congruence].
      apply Some_inj in Hsigned.
      specialize (Hsender_safety _ _ Hsender _ Hiom) as Heq_v.
      rewrite Hsigned in Heq_v. subst _v.
      eapply message_dependencies_are_sufficient in Hiom.
      revert Hiom.
      rewrite elem_of_elements in Hi; setoid_rewrite set_diff_iff in Hi.
      pose proof (Hdec := elem_of_dec_slow (C := Ci)).
      apply not_and_r in Hi as [Hi | Hi];
        [by elim Hi; apply elem_of_list_to_set; apply elem_of_enum |].
      apply dec_stable in Hi.
      apply can_emit_with_more; [by apply elem_of_elements |].
      intros dm Hdm.
      destruct Hv as [_ [_ [Hv _]]].
      destruct l as (sub_j, lj).
      destruct_dec_sig sub_j j Hj Heqsub_j.
      subst sub_j.
      simpl in Hv.
      unfold sub_IM in Hv. simpl in Hv.
      specialize (Hfull j _ _ _ Hv _ Hdm).
      exists j.
      unfold lift_sub_state.
      by rewrite (lift_sub_state_to_eq _ _ _ _ _ Hj).
Qed.

Lemma preloaded_non_byzantine_vlsm_lift
  : VLSM_embedding PreNonByzantine (pre_loaded_with_all_messages_vlsm (free_composite_vlsm IM))
      (lift_sub_label IM (elements selection_complement))
      (lift_sub_state IM (elements selection_complement)).
Proof.
  apply basic_VLSM_strong_embedding; [| | | done].
  - intros l s om [Hv _].
    by split; [apply lift_sub_valid |].
  - by intro; intros; rapply lift_sub_transition.
  - by intro; intros; apply (lift_sub_state_initial IM).
Qed.

Section sec_assuming_initial_messages_lift.

Context
  (Hfixed_non_byzantine_vlsm_lift_initial_message
    : weak_embedding_initial_message_preservation PreNonByzantine Fixed
    (lift_sub_state IM (elements selection_complement))).

(**
  Since <<FixedNonEquivocating>> is an [induced_validator] of <<Fixed>>,
  its initial_messages and validity are derived from valid messages and
  protocol validity of the larger composition; therefore, the following
  result becomes very important.
*)
Lemma fixed_non_byzantine_vlsm_lift_from_initial
  : VLSM_embedding PreNonByzantine Fixed
      (lift_sub_label IM (elements selection_complement))
      (lift_sub_state IM (elements selection_complement)).
Proof.
  apply basic_VLSM_embedding.
  - by intro; intros; apply fixed_non_byzantine_vlsm_lift_valid.
  - by intro; intros * []; rapply lift_sub_transition.
  - by intro; intros; apply (lift_sub_state_initial IM).
  - by intros; apply Hfixed_non_byzantine_vlsm_lift_initial_message.
Qed.

Lemma fixed_non_byzantine_incl_fixed_non_equivocating_from_initial
  : VLSM_incl PreNonByzantine FixedNonEquivocating.
Proof.
  apply basic_VLSM_incl.
  - intro; intros.
    exists (lift_sub_state IM (elements selection_complement) s).
    split.
    + by apply composite_state_sub_projection_lift_to.
    + by apply (lift_sub_state_initial IM).
  - by intro; intros; apply initial_message_is_valid.
  - intros l s om Hv HsY HomY.
    exists (lift_sub_label IM (elements selection_complement) l).
    exists (lift_sub_state IM (elements selection_complement) s).
    split.
    + by apply composite_label_sub_projection_option_lift.
    + by apply composite_state_sub_projection_lift.
    + apply @VLSM_embedding_input_valid; [| done].
      by apply fixed_non_byzantine_vlsm_lift_from_initial.
  - intros l s om s' om' [_ Ht].
    by apply induced_sub_projection_transition_preservation.
Qed.

Lemma fixed_non_byzantine_eq_fixed_non_equivocating_from_initial
  : VLSM_eq PreNonByzantine FixedNonEquivocating.
Proof.
  split.
  - by apply fixed_non_byzantine_incl_fixed_non_equivocating_from_initial.
  - by apply fixed_non_equivocating_incl_fixed_non_byzantine.
Qed.

End sec_assuming_initial_messages_lift.

Context
  (Hvalidator :
    forall i : index, i ∉ selection ->
    component_message_validator_prop IM (fixed_equivocation_constraint IM selection) i)
  .

Lemma validator_fixed_non_byzantine_vlsm_lift_initial_message
  : weak_embedding_initial_message_preservation PreNonByzantine Fixed
    (lift_sub_state IM (elements selection_complement)).
Proof.
  intros l s m Hv HsY HmX.
  destruct HmX as [[sub_i [[im Him] Heqm]] | Hseeded].
  - simpl in Heqm. subst.
    destruct_dec_sig sub_i i Hi Heqsub_i.
    subst. unfold sub_IM in Him. simpl in Him.
    clear -Him.
    cbn.
    apply initial_message_is_valid.
    by exists i, (exist _ m Him).
  - destruct Hseeded as [Hsigned [i [Hi [li [si Hpre_valid]]]]].
    apply set_diff_elim2 in Hi.
    by eapply Hvalidator.
Qed.

(**
  The VLSM corresponding to the induced projection from a fixed-set byzantine
  composition to the non-byzantine components is trace-equivalent to the VLSM
  corresponding to the induced projection from the composition of regular nodes
  under a fixed-set equivocation constraint to the same components.
*)
Lemma validator_fixed_non_byzantine_eq_fixed_non_equivocating
  : VLSM_eq PreNonByzantine FixedNonEquivocating.
Proof.
  apply fixed_non_byzantine_eq_fixed_non_equivocating_from_initial.
  by apply validator_fixed_non_byzantine_vlsm_lift_initial_message.
Qed.

(** ** The main result

  Assuming that the non-byzantine nodes are validators for the
  [fixed_equivocation_constraint] we give the following characterization of traces
  with the [fixed_byzantine_trace_alt_prop]erty in terms of equivocation:

  A trace has the [fixed_byzantine_trace_alt_prop]erty for a <<selection>> of
  byzantine nodes iff there exists a valid trace for the <<Fixed>>
  equivocation composition the projections of the two traces to the non-byzantine
  nodes, i.e., the nodes in the <<selection_complement>> coincide.
*)
Lemma validator_fixed_byzantine_traces_equivocation_char bis btr
  : fixed_byzantine_trace_alt_prop IM selection A sender bis btr <->
    exists eis etr,
      finite_valid_trace Fixed eis etr /\
      composite_state_sub_projection IM (elements selection_complement) eis =
      composite_state_sub_projection IM (elements selection_complement) bis /\
      finite_trace_sub_projection IM (elements selection_complement) etr =
      finite_trace_sub_projection IM (elements selection_complement) btr.
Proof.
  unfold fixed_byzantine_trace_alt_prop.
  split; intros Htr.
  - apply fixed_non_equivocating_traces_char.
    by apply (VLSM_eq_finite_valid_trace validator_fixed_non_byzantine_eq_fixed_non_equivocating).
  - apply (VLSM_eq_finite_valid_trace validator_fixed_non_byzantine_eq_fixed_non_equivocating).
    by apply fixed_non_equivocating_traces_char.
Qed.

End sec_validator_fixed_set_byzantine.

End sec_fixed_non_equivocating_vs_byzantine.

author: runtimeverification

repo: vlsm


text:
From Test Require Import tactic.

Section FOFProblem.

Variable Universe : Set.
Variable UniverseElement : Universe.

Variable wd_ : Universe -> Universe -> Prop.
Variable col_ : Universe -> Universe -> Universe -> Prop.

Variable col_swap1_1 : (forall A B C : Universe, (col_ A B C -> col_ B A C)).
Variable col_swap2_2 : (forall A B C : Universe, (col_ A B C -> col_ B C A)).
Variable col_triv_3 : (forall A B : Universe, col_ A B B).
Variable wd_swap_4 : (forall A B : Universe, (wd_ A B -> wd_ B A)).
Variable col_trans_5 : (forall P Q A B C : Universe, ((wd_ P Q /\ (col_ P Q A /\ (col_ P Q B /\ col_ P Q C))) -> col_ A B C)).

Theorem pipo_6 : (forall A1 A2 B1 B2 C1 C2 D1 D2 Q P R S T I : Universe, ((wd_ Q P /\ (wd_ Q R /\ (wd_ S Q /\ (wd_ T Q /\ (wd_ P S /\ (wd_ D1 D2 /\ (wd_ D2 S /\ (wd_ D1 S /\ (wd_ C1 C2 /\ (wd_ C2 T /\ (wd_ C1 T /\ (wd_ P R /\ (wd_ B1 B2 /\ (wd_ A1 A2 /\ (wd_ A1 D1 /\ (wd_ A1 D2 /\ (wd_ A2 D1 /\ (wd_ A2 D2 /\ (wd_ B1 C1 /\ (wd_ B1 C2 /\ (wd_ B2 C1 /\ (wd_ B2 C2 /\ (col_ A1 A2 Q /\ (col_ B1 B2 Q /\ (col_ A1 A2 P /\ (col_ C1 C2 P /\ (col_ B1 B2 R /\ (col_ D1 D2 R /\ (col_ C1 C2 S /\ (col_ D1 D2 T /\ (col_ I D1 D2 /\ (col_ P I S /\ col_ Q T S)))))))))))))))))))))))))))))))) -> col_ C1 C2 I)).
Proof.
  time tac.
Qed.

End FOFProblem.

author: janicicpredrag

repo: Larus

save_path: github-repos/coq/janicicpredrag-Larus


text:
Require Import BinNat.
Require Import Bool.Bool.
Require Import Lia.
Require Import Program.Wf.
Require Import Program.

From Proyecto Require Export Defs_Bin.
From Proyecto Require Export Defs_Misc.

(* Última optimización que vuelve a nuestros tries árboles Patricia. *)

(* Árboles Patricia *)
Inductive patriciaTree: Type :=
| empty : patriciaTree
| leaf: N -> nat -> patriciaTree
| trie: N -> N -> patriciaTree -> patriciaTree -> patriciaTree.

(* Tamaño de un Árbol Patricia *)
Fixpoint sizeP (p: patriciaTree) : nat :=
match p with
|empty => O
|leaf _ _ => S O
|trie x y t1 t2 => (sizeP t1) + (sizeP t2)
end.

(* Número de nodos en el árbol Patricia *)
Fixpoint nodes (p:patriciaTree) : nat :=
match p with
|empty => O
| leaf _ _ => S O
| trie x y t1 t2 => S ((nodes t1) + (nodes t2))
end.

(* Nueva función de búsqueda
 * Igual a la del caso pasado, solo que ahora los nodos guardan el prefijo
 * común de sus hijos. *)
Fixpoint lookup (k: N) (t: patriciaTree) : option nat :=
match t with
| empty => None
| leaf j x => if (N.eqb j k) then Some x
              else None
| trie p m t0 t1 => if (negb (matchPrefix k p m)) then None
                    else if (zeroBit k m) then lookup k t0
                         else lookup k t1
end.

(* Función de búsqueda equivalente a la primera pero un poco más eficiente. *)
Fixpoint lookup2 (k: N) (t:patriciaTree) :option nat :=
match t with
| empty => None
| leaf j x => if (N.eqb j k) then Some x
              else None
| trie p m t0 t1 => if (zeroBit k m) then lookup2 k t0
                         else lookup2 k t1
end.

(* Nuevo constructor inteligente. *)
Definition br (p m: N) (p1 p2: patriciaTree) : patriciaTree :=
match p1, p2 with
| empty, _ => p2
| _, empty => p1
| _, _ => trie p m p1 p2
end.

(* Función que une dos árboles con prefijos incompatibles *)
Definition join (p0 p1: N) (t0 t1: patriciaTree) : patriciaTree :=
let m := branchingBit p0 p1 in
if zeroBit p0 m then trie (mask p0 m) m t0 t1
else trie (mask p0 m) m t1 t0.

(* Función de inserción
 * Parámetros:
 * c - función a aplicar en caso de que la llave ya tenga elemento.
 * k - llave
 * x - número a insertar
 * t - árbol *)
Fixpoint insert (c : nat -> nat -> nat) (k: N) (x: nat) (t: patriciaTree) :=
match t with
| empty => leaf k x
| leaf j y => if (N.eqb j k) then leaf k (c x y)
              else join k j (leaf k x) t
| trie p m t0 t1 => if (matchPrefix k p m) then
                       if (zeroBit k m) then trie p m (insert c k x t0) t1
                       else trie p m t0 (insert c k x t1)
                    else join k p (leaf k x) t
end.

(* Un árbol es correcto si y solo si es el vacío o se construyó por medio
   de inserts. *)
Inductive correct: patriciaTree -> Prop :=
| corrempty : correct empty
| corrins: forall c k x t, correct t -> correct (insert c k x t).

(* Subárbol izquierdo *)
Definition left (t: patriciaTree) : patriciaTree :=
match t with
|empty => empty
|leaf _ _ => empty
|trie _ _ t1 _ => t1
end.

(* Subárbol derecho *)
Definition right (t: patriciaTree) : patriciaTree :=
match t with
|empty => empty
|leaf _ _ => empty
|trie _ _ _ t2 => t2
end.

(* Función de combinación.
   Usamos la medida de número de nodos para decirle a Coq que los
   argumentos sí se decrementan
 * Parámetros:
 * c - función a aplicar en caso de que la llave ya tenga elemento.
 * s t - árboles *)
Program Fixpoint merge (c : nat -> nat -> nat) (s t: patriciaTree) {measure ((nodes s) + (nodes t))} : patriciaTree :=
match s, t with
| empty, _ => t
| _, empty => s
| leaf k x, _ => insert c k x t
| _, leaf k x => insert (swap c) k x t
| trie p m s0 s1, trie q n t0 t1 => if (N.eqb m n) && (N.eqb p q)
                                    (* Los árboles comparten prefijo *)
                                    then trie p m (merge c s0 t0) (merge c s1 t1)
                                    else if (N.ltb m n) && (matchPrefix q p m)
                                    (* Caso en que q contiene a p *)
                                         then if (zeroBit q m)
                                              then br p m (merge c s0 t) s1
                                              else br p m s0 (merge c s1 t)
                                         else if (N.ltb n m) && (matchPrefix p q n)
                                              then if (zeroBit p n)
                                                   then br q n (merge c s t0) t1
                                                   else br q n t0 (merge c s t1)
                                              else join p q s t
end.
Next Obligation.
simpl.
lia.
Qed.
Next Obligation.
simpl.
lia.
Qed.
Next Obligation.
simpl.
lia.
Qed.
Next Obligation.
simpl.
lia.
Qed.
Next Obligation.
simpl.
lia.
Qed.
Next Obligation.
simpl.
lia.
Qed.
Next Obligation.
split.
- intros.
  intro.
  destruct H3.
  inversion H3.
- intros.
  intro.
  destruct H3.
  inversion H3.
Defined.

Theorem prueba: forall t1 t2 c, t1 <> empty -> merge c t1 t2 <> empty.
Proof.
unfold merge.
unfold merge_func.
Admitted.

repo: CoqPatriciaTrees


text:
(*Proof A \/ B -> A \/ C -> A \/ (B /\ C)*)

Theorem Ex06 (A B C : Prop): A \/ B -> A \/ C -> A \/ (B /\ C).
Proof.
  intros.
  destruct H.
  + left.
    exact H.
  + destruct H0.
    - left.
      exact H0.
    - right.
      split.
      * exact H.
      * exact H0.
Qed.

author: SvenWille

repo: CoqLogicExercises


text:
Require Import list_examples.

Require Import ZArith.
Require Import List.

(*
int sum_iterative(struct listNode* x)
//@ rule <k> $ => return sum(A); ...</k> <heap>... list(x)(A) ...</heap>
{
  int s;

  s = 0;
  /*@ inv <heap>... lseg(old(x), x)(?A1), list(x)(?A2) ...</heap>
          /\ A = ?A1 @ ?A2 /\ s = sum(?A1) */
  while (x != NULL) {
    s += x->val;
    x = x->next;
  }

  return s;
}
*)

Open Scope Z.

Definition sum_loop :=
  (SWhile ("x" <> 0)
         (Seq ("s" <- "s" + ELoad "x")
              ("x" <- ELoad ("x" + 1))))%code.

Definition sum_code :=
 (Seq ("s" <- 0)
 (Seq sum_loop
      (SReturn "s")))%code.

Inductive sum_spec : kcfg -> (kcfg -> Prop) -> Prop :=
  sum_claim :
    forall c, kcell c = kra (KStmt sum_code) kdot ->
    forall xv sv, store c ~= "x" s|-> KInt xv :* "s" s|-> KInt sv ->
    forall l P, heap c |= rep_list l xv :* P->
      sum_spec c (returning c (sum l))
 |loop_claim :
    forall c, kcell c = kra (KStmt sum_loop) (kra (KStmt (SReturn (EVar "s"))) kdot) ->
    forall xv sv, store c ~= "x" s|-> KInt xv :* "s" s|-> KInt sv ->
    forall l P, heap c |= rep_list l xv :* P ->
      sum_spec c (returning c (sv + sum l)).

Lemma sum_proof : sound kstep sum_spec.
Proof.
list_solver.
Qed.

author: Formal-Systems-Laboratory

repo: coinduction


text:
Require Import Pointed WildCat.
Require Import Algebra.Groups.
Require Import Modalities.ReflectiveSubuniverse.
Require Import Homotopy.Suspension.
Require Import Homotopy.ClassifyingSpace.
Require Import Homotopy.HomotopyGroup.

Local Open Scope trunc_scope.
Local Open Scope pointed_scope.
Import ClassifyingSpaceNotation.

(** In this file we show that the fundamental group of a bouquet of circles indexed by a type S is the free group on that type S. We begin by defining S-indexed wedges of circles as the suspension of the pointification of S. *)

Section AssumeUnivalence.

  Context `{Univalence}.

  (** An S-indexed wedge of circles a.k.a a bouquet can be defined as the suspension of the pointification of S. *)
  Definition Bouquet (S : Type) : pType := psusp (pointify S).

  Global Instance isconnected_bouquet (S : Type)
    : IsConnected 0 (Bouquet S).
  Proof.
    rapply isconnected_susp.
    rapply contr_inhabited_hprop.
    exact (tr pt).
  Defined.

  (** We can directly prove that it satisfies the desired equivalence together with naturality in the second argument. *)
  Lemma natequiv_pi1bouquet_rec (S : Type)
    : NatEquiv
        (opyon (Pi 1 (Bouquet S)))
        (opyon S o group_type).
  Proof.
    (** Pointify *)
    nrefine (natequiv_compose _ _).
    1: refine (natequiv_prewhisker (natequiv_pointify_r S) ptype_group).
    (** Post-compose with [pequiv_loops_bg_g] *)
    nrefine (natequiv_compose _ _).
1: rapply (natequiv_postwhisker _ (natequiv_inverse _ _ natequiv_g_loops_bg)).
    (** Loop-susp adjoint *)
    nrefine (natequiv_compose _ _).
    1: refine (natequiv_prewhisker
      (natequiv_loop_susp_adjoint_r (pointify S)) B).
    (** Pi1-BG adjunction *)
    rapply natequiv_bg_pi1_adjoint.
  Defined.

  (** For the rest of this file, we don't need to unfold this. *)
  Local Opaque natequiv_pi1bouquet_rec.

  Theorem equiv_pi1bouquet_rec (S : Type) (G : Group)
    : (Pi 1 (Bouquet S) $-> G) <~> (S -> G).
  Proof.
    apply natequiv_pi1bouquet_rec.
  Defined.

  Global Instance is1natural_equiv_pi1bouquet_rec (S : Type)
    : Is1Natural
        (opyon (Pi 1 (Bouquet S)))
        (opyon S o group_type)
        (fun G => equiv_pi1bouquet_rec S G).
  Proof.
    rapply (is1natural_natequiv _ _ (natequiv_pi1bouquet_rec _)).
  Defined.

  (** We can define the inclusion map by using the previous equivalence on the identity group homomorphism. *)
  Definition pi1bouquet_incl (S : Type)
    : S -> Pi 1 (Bouquet S).
  Proof.
    rapply equiv_pi1bouquet_rec.
    apply grp_homo_id.
  Defined.

  (** The fundemental group of an S-bouquet is the free group on S. *)
  Global Instance isfreegroupon_pi1bouquet (S : Type)
    : IsFreeGroupOn S (Pi 1 (Bouquet S)) (pi1bouquet_incl S).
  Proof.
    apply equiv_isfreegroupon_isequiv_precomp.
    intro G.
    snrapply isequiv_homotopic'.
    1: apply equiv_pi1bouquet_rec.
    intros f.
    refine (_ @ @is1natural_equiv_pi1bouquet_rec S _ _ f grp_homo_id).
    simpl; f_ap; symmetry.
    rapply (cat_idr_strong f).
  Defined.

End AssumeUnivalence.


text:
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(**** Tests of Field with real numbers ****)

Require Import Reals RealField.
Open Scope R_scope.

(* Example 1 *)
Goal
forall eps : R,
eps * (1 / (2 + 2)) + eps * (1 / (2 + 2)) = eps * (1 / 2).
Proof.
  intros.
   field.
Qed.

(* Example 2 *)
Goal
forall (f g : R -> R) (x0 x1 : R),
(f x1 - f x0) * (1 / (x1 - x0)) + (g x1 - g x0) * (1 / (x1 - x0)) =
(f x1 + g x1 - (f x0 + g x0)) * (1 / (x1 - x0)).
Proof.
  intros.
   field.
Abort.

(* Example 3 *)
Goal forall a b : R, 1 / (a * b) * (1 / (1 / b)) = 1 / a.
Proof.
  intros.
   field.
Abort.

Goal forall a b : R, 1 / (a * b) * (1 / 1 / b) = 1 / a.
Proof.
  intros.
   field_simplify_eq.
Abort.

Goal forall a b : R, 1 / (a * b) * (1 / 1 / b) = 1 / a.
Proof.
  intros.
   field_simplify (1 / (a * b) * (1 / 1 / b)).
Abort.

(* Example 4 *)
Goal
forall a b : R, a <> 0 -> b <> 0 -> 1 / (a * b) / (1 / b) = 1 / a.
Proof.
  intros.
   field; auto.
Qed.

(* Example 5 *)
Goal forall a : R, 1 = 1 * (1 / a) * a.
Proof.
  intros.
   field.
Abort.

(* Example 6 *)
Goal forall a b : R, b = b * / a * a.
Proof.
  intros.
   field.
Abort.

(* Example 7 *)
Goal forall a b : R, b = b * (1 / a) * a.
Proof.
  intros.
   field.
Abort.

(* Example 8 *)
Goal forall x y : R,
  x * (1 / x + x / (x + y)) =
  - (1 / y) * y * (- (x * (x / (x + y))) - 1).
Proof.
  intros.
   field.
Abort.

(* Example 9 *)
Goal forall a b : R, 1 / (a * b) * (1 / 1 / b) = 1 / a -> False.
Proof.
intros.
field_simplify_eq in H.
Abort.

repo: Coq-misc


text:
(** * Auto: More Automation *)

Set Warnings "-notation-overridden,-parsing".
Require Import Coq.omega.Omega.
From LF Require Import Maps.
From LF Require Import Imp.

(** Up to now, we've used the more manual part of Coq's tactic
    facilities.  In this chapter, we'll learn more about some of Coq's
    powerful automation features: proof search via the [auto] tactic,
    automated forward reasoning via the [Ltac] hypothesis matching
    machinery, and deferred instantiation of existential variables
    using [eapply] and [eauto].  Using these features together with
    Ltac's scripting facilities will enable us to make our proofs
    startlingly short!  Used properly, they can also make proofs more
    maintainable and robust to changes in underlying definitions.  A
    deeper treatment of [auto] and [eauto] can be found in the
    [UseAuto] chapter in _Programming Language Foundations_.

    There's another major category of automation we haven't discussed
    much yet, namely built-in decision procedures for specific kinds
    of problems: [omega] is one example, but there are others.  This
    topic will be deferred for a while longer.

    Our motivating example will be this proof, repeated with just a
    few small changes from the [Imp] chapter.  We will simplify
    this proof in several stages. *)

(** First, define a little Ltac macro to compress a common
    pattern into a single command. *)
Ltac inv H := inversion H; subst; clear H.

Theorem ceval_deterministic: forall c st st1 st2,
     c / st \\ st1  ->
     c / st \\ st2 ->
     st1 = st2.
Proof.
  intros c st st1 st2 E1 E2;
  generalize dependent st2;
  induction E1; intros st2 E2; inv E2.
  - (* E_Skip *) reflexivity.
  - (* E_Ass *) reflexivity.
  - (* E_Seq *)
    assert (st' = st'0) as EQ1.
    { (* Proof of assertion *) apply IHE1_1; apply H1. }
    subst st'0.
    apply IHE1_2. assumption.
  (* E_IfTrue *)
  - (* b evaluates to true *)
    apply IHE1. assumption.
  - (* b evaluates to false (contradiction) *)
    rewrite H in H5. inversion H5.
  (* E_IfFalse *)
  - (* b evaluates to true (contradiction) *)
    rewrite H in H5. inversion H5.
  - (* b evaluates to false *)
    apply IHE1. assumption.
  (* E_WhileFalse *)
  - (* b evaluates to false *)
    reflexivity.
  - (* b evaluates to true (contradiction) *)
    rewrite H in H2. inversion H2.
  (* E_WhileTrue *)
  - (* b evaluates to false (contradiction) *)
    rewrite H in H4. inversion H4.
  - (* b evaluates to true *)
    assert (st' = st'0) as EQ1.
    { (* Proof of assertion *) apply IHE1_1; assumption. }
    subst st'0.
    apply IHE1_2. assumption.  Qed.

(* ################################################################# *)
(** * The [auto] Tactic *)

(** Thus far, our proof scripts mostly apply relevant hypotheses or
    lemmas by name, and one at a time. *)

Example auto_example_1 : forall (P Q R: Prop),
  (P -> Q) -> (Q -> R) -> P -> R.
Proof.
  intros P Q R H1 H2 H3.
  apply H2. apply H1. assumption.
Qed.

(** The [auto] tactic frees us from this drudgery by _searching_ for a
    sequence of applications that will prove the goal: *)

Example auto_example_1' : forall (P Q R: Prop),
  (P -> Q) -> (Q -> R) -> P -> R.
Proof.
  auto.
Qed.

(** The [auto] tactic solves goals that are solvable by any combination of
     - [intros] and
     - [apply] (of hypotheses from the local context, by default). *)

(** Using [auto] is always "safe" in the sense that it will never fail
    and will never change the proof state: either it completely solves
    the current goal, or it does nothing. *)

(** Here is a more interesting example showing [auto]'s power: *)

Example auto_example_2 : forall P Q R S T U : Prop,
  (P -> Q) ->
  (P -> R) ->
  (T -> R) ->
  (S -> T -> U) ->
  ((P->Q) -> (P->S)) ->
  T ->
  P ->
  U.
Proof. auto. Qed.

(** Proof search could, in principle, take an arbitrarily long time,
    so there are limits to how far [auto] will search by default. *)

Example auto_example_3 : forall (P Q R S T U: Prop),
  (P -> Q) ->
  (Q -> R) ->
  (R -> S) ->
  (S -> T) ->
  (T -> U) ->
  P ->
  U.
Proof.
  (* When it cannot solve the goal, [auto] does nothing *)
  auto.
  (* Optional argument says how deep to search (default is 5) *)
  auto 6.
Qed.

(** When searching for potential proofs of the current goal,
    [auto] considers the hypotheses in the current context together
    with a _hint database_ of other lemmas and constructors.  Some
    common lemmas about equality and logical operators are installed
    in this hint database by default. *)

Example auto_example_4 : forall P Q R : Prop,
  Q ->
  (Q -> R) ->
  P \/ (Q /\ R).
Proof. auto. Qed.

(** We can extend the hint database just for the purposes of one
    application of [auto] by writing "[auto using ...]". *)

Lemma le_antisym : forall n m: nat, (n <= m /\ m <= n) -> n = m.
Proof. intros. omega. Qed.

Example auto_example_6 : forall n m p : nat,
  (n <= p -> (n <= m /\ m <= n)) ->
  n <= p ->
  n = m.
Proof.
  intros.
  auto using le_antisym.
Qed.

(** Of course, in any given development there will probably be
    some specific constructors and lemmas that are used very often in
    proofs.  We can add these to the global hint database by writing

      Hint Resolve T.

    at the top level, where [T] is a top-level theorem or a
    constructor of an inductively defined proposition (i.e., anything
    whose type is an implication).  As a shorthand, we can write

      Hint Constructors c.

    to tell Coq to do a [Hint Resolve] for _all_ of the constructors
    from the inductive definition of [c].

    It is also sometimes necessary to add

      Hint Unfold d.

    where [d] is a defined symbol, so that [auto] knows to expand uses
    of [d], thus enabling further possibilities for applying lemmas that
    it knows about. *)

(** It is also possible to define specialized hint databases that can
    be activated only when needed.  See the Coq reference manual for
    more. *)

Hint Resolve le_antisym.

Example auto_example_6' : forall n m p : nat,
  (n<= p -> (n <= m /\ m <= n)) ->
  n <= p ->
  n = m.
Proof.
  intros.
  auto. (* picks up hint from database *)
Qed.

Definition is_fortytwo x := (x = 42).

Example auto_example_7: forall x,
  (x <= 42 /\ 42 <= x) -> is_fortytwo x.
Proof.
  auto.  (* does nothing *)
Abort.

Hint Unfold is_fortytwo.

Example auto_example_7' : forall x,
  (x <= 42 /\ 42 <= x) -> is_fortytwo x.
Proof. auto. Qed.

(** Let's take a first pass over [ceval_deterministic] to simplify the
    proof script. *)

Theorem ceval_deterministic': forall c st st1 st2,
     c / st \\ st1  ->
     c / st \\ st2 ->
     st1 = st2.
Proof.
  intros c st st1 st2 E1 E2.
  generalize dependent st2;
       induction E1; intros st2 E2; inv E2; auto.
  - (* E_Seq *)
    assert (st' = st'0) as EQ1 by auto.
    subst st'0.
    auto.
  - (* E_IfTrue *)
    + (* b evaluates to false (contradiction) *)
      rewrite H in H5. inversion H5.
  - (* E_IfFalse *)
    + (* b evaluates to true (contradiction) *)
      rewrite H in H5. inversion H5.
  - (* E_WhileFalse *)
    + (* b evaluates to true (contradiction) *)
      rewrite H in H2. inversion H2.
  (* E_WhileTrue *)
  - (* b evaluates to false (contradiction) *)
    rewrite H in H4. inversion H4.
  - (* b evaluates to true *)
    assert (st' = st'0) as EQ1 by auto.
    subst st'0.
    auto.
Qed.

(** When we are using a particular tactic many times in a proof, we
    can use a variant of the [Proof] command to make that tactic into
    a default within the proof.  Saying [Proof with t] (where [t] is
    an arbitrary tactic) allows us to use [t1...] as a shorthand for
    [t1;t] within the proof.  As an illustration, here is an alternate
    version of the previous proof, using [Proof with auto]. *)

Theorem ceval_deterministic'_alt: forall c st st1 st2,
     c / st \\ st1  ->
     c / st \\ st2 ->
     st1 = st2.
Proof with auto.
  intros c st st1 st2 E1 E2;
  generalize dependent st2;
  induction E1;
           intros st2 E2; inv E2...
  - (* E_Seq *)
    assert (st' = st'0) as EQ1...
    subst st'0...
  - (* E_IfTrue *)
    + (* b evaluates to false (contradiction) *)
      rewrite H in H5. inversion H5.
  - (* E_IfFalse *)
    + (* b evaluates to true (contradiction) *)
      rewrite H in H5. inversion H5.
  - (* E_WhileFalse *)
    + (* b evaluates to true (contradiction) *)
      rewrite H in H2. inversion H2.
  (* E_WhileTrue *)
  - (* b evaluates to false (contradiction) *)
    rewrite H in H4. inversion H4.
  - (* b evaluates to true *)
    assert (st' = st'0) as EQ1...
    subst st'0...
Qed.

(* ################################################################# *)
(** * Searching For Hypotheses *)

(** The proof has become simpler, but there is still an annoying
    amount of repetition. Let's start by tackling the contradiction
    cases. Each of them occurs in a situation where we have both

      H1: beval st b = false

    and

      H2: beval st b = true

    as hypotheses.  The contradiction is evident, but demonstrating it
    is a little complicated: we have to locate the two hypotheses [H1]
    and [H2] and do a [rewrite] following by an [inversion].  We'd
    like to automate this process.

    (In fact, Coq has a built-in tactic [congruence] that will do the
    job in this case.  But we'll ignore the existence of this tactic
    for now, in order to demonstrate how to build forward search
    tactics by hand.)

    As a first step, we can abstract out the piece of script in
    question by writing a little function in Ltac. *)

Ltac rwinv H1 H2 := rewrite H1 in H2; inv H2.

Theorem ceval_deterministic'': forall c st st1 st2,
     c / st \\ st1  ->
     c / st \\ st2 ->
     st1 = st2.
Proof.
  intros c st st1 st2 E1 E2.
  generalize dependent st2;
  induction E1; intros st2 E2; inv E2; auto.
  - (* E_Seq *)
    assert (st' = st'0) as EQ1 by auto.
    subst st'0.
    auto.
  - (* E_IfTrue *)
    + (* b evaluates to false (contradiction) *)
      rwinv H H5.
  - (* E_IfFalse *)
    + (* b evaluates to true (contradiction) *)
      rwinv H H5.
  - (* E_WhileFalse *)
    + (* b evaluates to true (contradiction) *)
      rwinv H H2.
  (* E_WhileTrue *)
  - (* b evaluates to false (contradiction) *)
    rwinv H H4.
  - (* b evaluates to true *)
    assert (st' = st'0) as EQ1 by auto.
    subst st'0.
    auto. Qed.

(** That was a bit better, but we really want Coq to discover the
    relevant hypotheses for us.  We can do this by using the [match
    goal] facility of Ltac. *)

Ltac find_rwinv :=
  match goal with
    H1: ?E = true,
    H2: ?E = false
    |- _ => rwinv H1 H2
  end.

(** This [match goal] looks for two distinct hypotheses that
    have the form of equalities, with the same arbitrary expression
    [E] on the left and with conflicting boolean values on the right.
    If such hypotheses are found, it binds [H1] and [H2] to their
    names and applies the [rwinv] tactic to [H1] and [H2].

    Adding this tactic to the ones that we invoke in each case of the
    induction handles all of the contradictory cases. *)

Theorem ceval_deterministic''': forall c st st1 st2,
     c / st \\ st1  ->
     c / st \\ st2 ->
     st1 = st2.
Proof.
  intros c st st1 st2 E1 E2.
  generalize dependent st2;
  induction E1; intros st2 E2; inv E2; try find_rwinv; auto.
  - (* E_Seq *)
    assert (st' = st'0) as EQ1 by auto.
    subst st'0.
    auto.
  - (* E_WhileTrue *)
    + (* b evaluates to true *)
      assert (st' = st'0) as EQ1 by auto.
      subst st'0.
      auto. Qed.

(** Let's see about the remaining cases. Each of them involves
    applying a conditional hypothesis to extract an equality.
    Currently we have phrased these as assertions, so that we have to
    predict what the resulting equality will be (although we can then
    use [auto] to prove it).  An alternative is to pick the relevant
    hypotheses to use and then [rewrite] with them, as follows: *)

Theorem ceval_deterministic'''': forall c st st1 st2,
     c / st \\ st1  ->
     c / st \\ st2 ->
     st1 = st2.
Proof.
  intros c st st1 st2 E1 E2.
  generalize dependent st2;
  induction E1; intros st2 E2; inv E2; try find_rwinv; auto.
  - (* E_Seq *)
    rewrite (IHE1_1 st'0 H1) in *. auto.
  - (* E_WhileTrue *)
    + (* b evaluates to true *)
      rewrite (IHE1_1 st'0 H3) in *. auto. Qed.

(** Now we can automate the task of finding the relevant hypotheses to
    rewrite with. *)

Ltac find_eqn :=
  match goal with
    H1: forall x, ?P x -> ?L = ?R,
    H2: ?P ?X
    |- _ => rewrite (H1 X H2) in *
  end.

(** The pattern [forall x, ?P x -> ?L = ?R] matches any hypothesis of
    the form "for all [x], _some property of [x]_ implies _some
    equality_."  The property of [x] is bound to the pattern variable
    [P], and the left- and right-hand sides of the equality are bound
    to [L] and [R].  The name of this hypothesis is bound to [H1].
    Then the pattern [?P ?X] matches any hypothesis that provides
    evidence that [P] holds for some concrete [X].  If both patterns
    succeed, we apply the [rewrite] tactic (instantiating the
    quantified [x] with [X] and providing [H2] as the required
    evidence for [P X]) in all hypotheses and the goal.

    One problem remains: in general, there may be several pairs of
    hypotheses that have the right general form, and it seems tricky
    to pick out the ones we actually need.  A key trick is to realize
    that we can _try them all_!  Here's how this works:

    - each execution of [match goal] will keep trying to find a valid
      pair of hypotheses until the tactic on the RHS of the match
      succeeds; if there are no such pairs, it fails;
    - [rewrite] will fail given a trivial equation of the form [X = X];
    - we can wrap the whole thing in a [repeat], which will keep doing
      useful rewrites until only trivial ones are left. *)

Theorem ceval_deterministic''''': forall c st st1 st2,
     c / st \\ st1  ->
     c / st \\ st2 ->
     st1 = st2.
Proof.
  intros c st st1 st2 E1 E2.
  generalize dependent st2;
  induction E1; intros st2 E2; inv E2; try find_rwinv;
    repeat find_eqn; auto.
Qed.

(** The big payoff in this approach is that our proof script should be
    more robust in the face of modest changes to our language.  To
    test whether it really is, let's try adding a [REPEAT] command to
    the language. *)

Module Repeat.

Inductive com : Type :=
  | CSkip : com
  | CAsgn : string -> aexp -> com
  | CSeq : com -> com -> com
  | CIf : bexp -> com -> com -> com
  | CWhile : bexp -> com -> com
  | CRepeat : com -> bexp -> com.

(** [REPEAT] behaves like [WHILE], except that the loop guard is
    checked _after_ each execution of the body, with the loop
    repeating as long as the guard stays _false_.  Because of this,
    the body will always execute at least once. *)

Notation "'SKIP'" :=
  CSkip.
Notation "c1 ; c2" :=
  (CSeq c1 c2) (at level 80, right associativity).
Notation "X '::=' a" :=
  (CAsgn X a) (at level 60).
Notation "'WHILE' b 'DO' c 'END'" :=
  (CWhile b c) (at level 80, right associativity).
Notation "'IFB' e1 'THEN' e2 'ELSE' e3 'FI'" :=
  (CIf e1 e2 e3) (at level 80, right associativity).
Notation "'REPEAT' e1 'UNTIL' b2 'END'" :=
  (CRepeat e1 b2) (at level 80, right associativity).

Inductive ceval : state -> com -> state -> Prop :=
  | E_Skip : forall st,
      ceval st SKIP st
  | E_Ass  : forall st a1 n X,
      aeval st a1 = n ->
      ceval st (X ::= a1) (t_update st X n)
  | E_Seq : forall c1 c2 st st' st'',
      ceval st c1 st' ->
      ceval st' c2 st'' ->
      ceval st (c1 ; c2) st''
  | E_IfTrue : forall st st' b1 c1 c2,
      beval st b1 = true ->
      ceval st c1 st' ->
      ceval st (IFB b1 THEN c1 ELSE c2 FI) st'
  | E_IfFalse : forall st st' b1 c1 c2,
      beval st b1 = false ->
      ceval st c2 st' ->
      ceval st (IFB b1 THEN c1 ELSE c2 FI) st'
  | E_WhileFalse : forall b1 st c1,
      beval st b1 = false ->
      ceval st (WHILE b1 DO c1 END) st
  | E_WhileTrue : forall st st' st'' b1 c1,
      beval st b1 = true ->
      ceval st c1 st' ->
      ceval st' (WHILE b1 DO c1 END) st'' ->
      ceval st (WHILE b1 DO c1 END) st''
  | E_RepeatEnd : forall st st' b1 c1,
      ceval st c1 st' ->
      beval st' b1 = true ->
      ceval st (CRepeat c1 b1) st'
  | E_RepeatLoop : forall st st' st'' b1 c1,
      ceval st c1 st' ->
      beval st' b1 = false ->
      ceval st' (CRepeat c1 b1) st'' ->
      ceval st (CRepeat c1 b1) st''.

Notation "c1 '/' st '\\' st'" := (ceval st c1 st')
                                 (at level 40, st at level 39).

(** Our first attempt at the determinacy proof does not quite succeed:
    the [E_RepeatEnd] and [E_RepeatLoop] cases are not handled by our
    previous automation. *)

Theorem ceval_deterministic: forall c st st1 st2,
     c / st \\ st1  ->
     c / st \\ st2 ->
     st1 = st2.
Proof.
  intros c st st1 st2 E1 E2.
  generalize dependent st2;
  induction E1;
    intros st2 E2; inv E2; try find_rwinv; repeat find_eqn; auto.
  - (* E_RepeatEnd *)
    + (* b evaluates to false (contradiction) *)
       find_rwinv.
       (* oops: why didn't [find_rwinv] solve this for us already?
          answer: we did things in the wrong order. *)
  - (* E_RepeatLoop *)
     + (* b evaluates to true (contradiction) *)
        find_rwinv.
Qed.

(** Fortunately, to fix this, we just have to swap the invocations of
    [find_eqn] and [find_rwinv]. *)

Theorem ceval_deterministic': forall c st st1 st2,
     c / st \\ st1  ->
     c / st \\ st2 ->
     st1 = st2.
Proof.
  intros c st st1 st2 E1 E2.
  generalize dependent st2;
  induction E1;
    intros st2 E2; inv E2; repeat find_eqn; try find_rwinv; auto.
Qed.

End Repeat.

(** These examples just give a flavor of what "hyper-automation"
    can achieve in Coq.  The details of [match goal] are a bit
    tricky (and debugging scripts using it is, frankly, not very
    pleasant).  But it is well worth adding at least simple uses to
    your proofs, both to avoid tedium and to "future proof" them. *)

(* ================================================================= *)
(** ** The [eapply] and [eauto] variants *)

(** To close the chapter, we'll introduce one more convenient feature
    of Coq: its ability to delay instantiation of quantifiers.  To
    motivate this feature, recall this example from the [Imp]
    chapter: *)

Example ceval_example1:
    (X ::= 2;;
     IFB X <= 1
       THEN Y ::= 3
       ELSE Z ::= 4
     FI)
   / { --> 0 }
   \\ { X --> 2 ; Z --> 4 }.
Proof.
  (* We supply the intermediate state [st']... *)
  apply E_Seq with { X --> 2 }.
  - apply E_Ass. reflexivity.
  - apply E_IfFalse. reflexivity. apply E_Ass. reflexivity.
Qed.

(** In the first step of the proof, we had to explicitly provide a
    longish expression to help Coq instantiate a "hidden" argument to
    the [E_Seq] constructor.  This was needed because the definition
    of [E_Seq]...

          E_Seq : forall c1 c2 st st' st'',
            c1 / st  \\ st' ->
            c2 / st' \\ st'' ->
            (c1 ;; c2) / st \\ st''

   is quantified over a variable, [st'], that does not appear in its
   conclusion, so unifying its conclusion with the goal state doesn't
   help Coq find a suitable value for this variable.  If we leave
   out the [with], this step fails ("Error: Unable to find an
   instance for the variable [st']").

   What's silly about this error is that the appropriate value for [st']
   will actually become obvious in the very next step, where we apply
   [E_Ass].  If Coq could just wait until we get to this step, there
   would be no need to give the value explicitly.  This is exactly what
   the [eapply] tactic gives us: *)

Example ceval'_example1:
    (X ::= 2;;
     IFB X <= 1
       THEN Y ::= 3
       ELSE Z ::= 4
     FI)
   / { --> 0 }
   \\ { X --> 2 ; Z --> 4 }.
Proof.
  eapply E_Seq. (* 1 *)
  - apply E_Ass. (* 2 *)
    reflexivity. (* 3 *)
  - (* 4 *) apply E_IfFalse. reflexivity. apply E_Ass. reflexivity.
Qed.

(** The [eapply H] tactic behaves just like [apply H] except
    that, after it finishes unifying the goal state with the
    conclusion of [H], it does not bother to check whether all the
    variables that were introduced in the process have been given
    concrete values during unification.

    If you step through the proof above, you'll see that the goal
    state at position [1] mentions the _existential variable_ [?st']
    in both of the generated subgoals.  The next step (which gets us
    to position [2]) replaces [?st'] with a concrete value.  This new
    value contains a new existential variable [?n], which is
    instantiated in its turn by the following [reflexivity] step,
    position [3].  When we start working on the second
    subgoal (position [4]), we observe that the occurrence of [?st']
    in this subgoal has been replaced by the value that it was given
    during the first subgoal. *)

(** Several of the tactics that we've seen so far, including [exists],
    [constructor], and [auto], have [e...] variants.  For example,
    here's a proof using [eauto]: *)

Hint Constructors ceval.
Hint Transparent state.
Hint Transparent total_map.

Definition st12 := { X --> 1 ; Y --> 2 }.
Definition st21 := { X --> 2 ; Y --> 1 }.

Example eauto_example : exists s',
  (IFB X <= Y
    THEN Z ::= Y - X
    ELSE Y ::= X + Z
  FI) / st21 \\ s'.
Proof. eauto. Qed.

(** The [eauto] tactic works just like [auto], except that it uses
    [eapply] instead of [apply].

    Pro tip: One might think that, since [eapply] and [eauto] are more
    powerful than [apply] and [auto], it would be a good idea to use
    them all the time.  Unfortunately, they are also significantly
    slower -- especially [eauto].  Coq experts tend to use [apply] and
    [auto] most of the time, only switching to the [e] variants when
    the ordinary variants don't do the job. *)

author: neshkeev

repo: Logical-Foundations


text:
Require Export Coq.Program.Basics Coq.Classes.RelationClasses
        Coq.Lists.List Coq.Arith.PeanoNat
        Coq.micromega.Lia Coq.Arith.Compare_dec.
Export ListNotations.

Section Mapply.
  Context {A : Set}.

  Fixpoint mapply (m : nat) (f : A -> A) (a : A) : A :=
    match m with
    | O   => a
    | S m => f (mapply m f a)
    end.

  Lemma mapply_comm : forall m f a, mapply m f (f a) = f (mapply m f a).
  Proof.
    intro m; induction m as [| m ih];
      intros f a; cbn; f_equal; auto.
  Qed.

  Lemma mapply_id : forall (m : nat) (a : A),
      mapply m (fun a => a) a = a.
  Proof.
    intros m; induction m as [| m ih]; intro a; cbn; auto.
  Qed.
End Mapply.

Lemma mapply_plus : forall m n,
    mapply m S n = m + n.
Proof.
  intro m; induction m as [| m ih];
    intros n; cbn; f_equal; auto.
Qed.

Definition ext (ρ : nat -> nat) (X : nat) : nat :=
  match X with
  | O   => O
  | S n => S (ρ n)
  end.

Lemma mapply_ext : forall n x ρ,
    ext (mapply n ext ρ) (mapply n ext S x) = mapply n ext S (mapply n ext ρ x).
Proof.
  intro n; induction n as [| n ihn];
    intros x ρ; cbn; try reflexivity.
  destruct x as [| x]; cbn; try reflexivity || f_equal; auto.
Qed.

Infix "$" := apply (at level 41, right associativity).

Ltac inv H := inversion H; subst; clear H.

Ltac compare_destruct :=
  match goal with
  | |- context [le_lt_dec ?a ?b]
    => destruct (le_lt_dec a b) as [? | ?] eqn:?
  | |- context [lt_dec ?a ?b]
    => destruct (lt_dec a b) as [? | ?] eqn:?
  | |- context [lt_eq_lt_dec ?a ?b]
    => destruct (lt_eq_lt_dec a b) as [[? | ?] | ?] eqn:?
  | |- context [match ?n with 0 => _ | S _ => _ end]
    => destruct n as [| ?] eqn:?
  end.
(**[]*)

Ltac compare_destruct_star := repeat (compare_destruct; simpl).

Ltac clean_compare := compare_destruct_star; try lia; auto.

Ltac destroy_arith :=
  intros; simpl; clean_compare;
  try (f_equal; auto 2; lia).

(** * Binary Relations *)

Definition deterministic {A : Type} (R : A -> A -> Prop) : Prop :=
  forall a a1 a2, R a a1 -> R a a2 -> a1 = a2.

Ltac ind_det :=
  match goal with
  | |- deterministic _
    => intros ? ? a2 H1;
      generalize dependent a2;
      induction H1; intros ? H2; inv H2; auto
  end.
(**[]*)

(** Reflexive-Transitive Closure of a Relation. *)

Reserved Notation "a1 '~~>' a2" (at level 40).

Inductive refl_trans_closure {A : Type} (R : A -> A -> Prop) : A -> A -> Prop :=
| refl_closure a :
    a ~~>  a
| trans_closure a1 a2 a3 :
    R a1 a2 ->
    a2 ~~>  a3 ->
    a1 ~~>  a3
where "a1 '~~>' a2" := (refl_trans_closure _ a1 a2).
(**[]*)

Section ReflTransClosureProp.
  Context {A : Type}.
  Variable (R : A -> A -> Prop).

  Local Hint Constructors refl_trans_closure : core.

  Global Instance refl_trans_closure_reflexive
    : Reflexive (refl_trans_closure R).
  Proof using Type. auto 2. Qed.

  Lemma inject_trans_closure : forall a1 a2,
      R a1 a2 -> refl_trans_closure R a1 a2.
  Proof using Type. eauto 2. Qed.

  Global Instance refl_trans_closure_transitive
    : Transitive (refl_trans_closure R).
  Proof using Type.
    intros x y z Hxy Hyz; generalize dependent z.
    induction Hxy; intros z Hyz; eauto 3.
  Qed.

  Lemma trans_closure_r : forall a1 a2 a3,
      R a2 a3 ->
      refl_trans_closure R a1 a2 ->
      refl_trans_closure R a1 a3.
  Proof.
    intros a1 a2 a3 HR H12.
    transitivity a2; eauto 2.
  Qed.

  (** "Halting" condition. *)
  Definition halts_R (a : A) : Prop :=
    exists a', refl_trans_closure R a a' /\ forall a'', ~ R a' a''.
End ReflTransClosureProp.

Section NthError.
  Context {A : Type}.

  Lemma nth_error_nil : forall n, nth_error (@nil A) n = None.
  Proof. intros []; reflexivity. Qed.

  Hint Rewrite nth_error_nil : core.

  Lemma nth_error_length : forall (l : list A) n a,
      nth_error l n = Some a -> n < length l.
  Proof.
    intro l; induction l as [| h t IHt];
      intros [| n]; simpl; intros a H;
        autorewrite with core in *; try discriminate; try lia.
    apply IHt in H. lia.
  Qed.

  Lemma nth_error_app_plus : forall (l l' : list A) n,
      nth_error (l ++ l') (length l + n) = nth_error l' n.
  Proof.
    intros l l' n.
    rewrite nth_error_app2 by lia.
    f_equal; lia.
  Qed.

  Lemma nth_map : forall B (f : A -> B) l n a b,
      n < length l ->
      nth n (map f l) b = f (nth n l a).
  Proof.
    induction l as [| h t IHt];
      intros [| n] a b; simpl; intros; try lia; auto.
    apply IHt; lia.
  Qed.

  Lemma length_nth_error : forall (l : list A) n,
      n < length l -> exists a, nth_error l n = Some a.
  Proof.
    intro l; induction l as [| h t IHt];
      intros [| n] H; simpl in *; try lia; eauto.
    apply IHt. lia.
  Qed.
End NthError.

Section Forall2.
  Variables A B : Type.
  Variable R : A -> B -> Prop.

  Lemma Forall2_length : forall a b,
    Forall2 R a b -> length a = length b.
  Proof.
    intros a b H; induction H; simpl; auto.
  Qed.

  Lemma Forall2_impl : forall (Q : A -> B -> Prop) a b,
      (forall a b, R a b -> Q a b) ->
      Forall2 R a b -> Forall2 Q a b.
  Proof.
    intros Q a b H HP;
      induction HP; auto.
  Qed.

  Lemma Forall2_nth_error : forall la lb,
      Forall2 R la lb ->
      forall n a b, nth_error la n = Some a ->
               nth_error lb n = Some b ->
               R a b.
  Proof.
    intros la lb HR; induction HR;
      intros [| n] a b Hntha Hnthb;
      simpl in *; try discriminate.
    - inv Hntha; inv Hnthb. assumption.
    - pose proof IHHR _ _ _ Hntha Hnthb.
      assumption.
  Qed.
End Forall2.

Section AccLemmas.
  Local Hint Constructors Acc : core.

  Lemma acc_pres : forall A B (f : A -> B) (R : A -> A -> Prop) (Q : B -> B -> Prop),
    (forall a1 a2, R a1 a2 -> Q (f a1) (f a2)) ->
    forall a, Acc Q (f a) -> Acc R a.
  Proof.
    intros A B f R Q Hmap a HQ.
    remember (f a) as fa eqn:Heqfa.
    generalize dependent a.
    induction HQ; intros a Heqfa; subst; eauto.
  Qed.

  Lemma Acc_ind2 :
    forall A B (RA : A -> A -> Prop) (RB : B -> B -> Prop) (P : A -> B -> Prop),
      (forall a b, (forall a', RA a' a -> P a' b) ->
              (forall b', RB b' b -> P a b') -> P a b) ->
      forall a b, Acc RA a -> Acc RB b -> P a b.
  Proof.
    intros A B R Q P H a b HA.
    generalize dependent b.
    induction HA; intros b HB;
      induction HB; eauto.
  Qed.
End AccLemmas.

Definition obind {A B : Set} (o : option A) (ƒ : A -> option B) : option B :=
  match o with
  | None => None
  | Some a => ƒ a
  end.

Notation "o '>>=' f" := (obind o f) (at level 50, left associativity).
Notation "o '>>|' f" := (option_map f o) (at level 50, left associativity).
Notation "'let*' x ':=' c1 'in' c2"
  := (obind c1 (fun x => c2))
       (at level 61, x pattern,
         format "'let*'  x  ':='  c1  'in' '//' c2", c1 at next level,
         right associativity).
Notation "'let*' ' x ':=' c1 'in' c2"
  := (obind c1 (fun x => c2))
       (at level 61, x pattern,
         format "'let*'  ' x  ':='  c1  'in' '//' c2", c1 at next level,
         right associativity).

Ltac match_some :=
  match goal with
  | h: match ?t with
       | Some _ => _
       | None => None
       end = Some _
    |- _ => destruct t eqn:?; try discriminate
  end.

Ltac some_inv :=
  match goal with
  | h: Some _ = Some _ |- _ => inv h
  end.

author: rudynicolop

repo: Lambda-Calculi-Coq


text:
(** * MOV instruction *)
Require Import x86proved.x86.instrrules.core.
Import x86.instrrules.core.instrruleconfig.

Require Import x86proved.spectac (* for [unhideReg] *).

(** ** Generic rule *)
Lemma MOV_rule d ds oldv:
  |-- specAtDstSrc ds (fun V v =>
      basic (V oldv) (MOVOP d ds) (V v)).
Proof. do_instrrule_triple. Qed.

(** We make this rule an instance of the typeclass, and leave
    unfolding things like [specAtDstSrc] to the getter tactic
    [get_instrrule_of]. *)
Global Instance: forall d ds, instrrule (MOVOP d ds) := @MOV_rule.

(** ** Register to register *)
Lemma MOV_RR_rule (r1 r2:Reg) v1 v2:
  |-- basic (r1 ~= v1 ** r2 ~= v2) (MOV r1, r2) (r1 ~= v2 ** r2 ~= v2).
Proof. basic apply *. Qed.

Lemma MOV_RanyR_rule (r1 r2:Reg) v2:
  |-- basic (r1? ** r2 ~= v2) (MOV r1, r2) (r1 ~= v2 ** r2 ~= v2).
Proof. unhideReg r1 => old. basic apply *. Qed.

(** ** Immediate to register *)
Lemma MOV_RI_rule (r:Reg) (v1 v2:DWORD) :
  |-- basic (r ~= v1) (MOV r, v2) (r ~= v2).
Proof. basic apply *. Qed.

Lemma MOV_RanyI_rule (r:Reg) (v2:DWORD) :
  |-- basic r? (MOV r, v2) (r ~= v2).
Proof. unhideReg r => old. basic apply *. Qed.

(** ** Memory to register *)
Lemma MOV_RM_rule (pd:DWORD) (r1 r2:Reg) offset (v1 v2: DWORD) :
  |-- basic (r1 ~= v1 ** r2 ~= pd ** pd +# offset :-> v2)
            (MOV r1, [r2 + offset])
            (r1 ~= v2 ** r2 ~= pd ** pd +# offset :-> v2).
Proof. basic apply *. Qed.

Lemma MOV_RanyM_rule (pd:DWORD) (r1 r2:Reg) offset (v2: DWORD) :
  |-- basic (r1? ** r2 ~= pd ** pd +# offset :-> v2)
            (MOV r1, [r2 + offset])
            (r1 ~= v2 ** r2 ~= pd ** pd +# offset :-> v2).
Proof. unhideReg r1 => old. basic apply *. Qed.

Lemma MOV_RanyInd_rule (pd:DWORD) (r1:Reg) (v2: DWORD) :
  |-- basic (r1? ** pd :-> v2)
            (MOV r1, [pd])
            (r1 ~= v2 ** pd :-> v2).
Proof. unhideReg r1 => old. basic apply *. Qed.

Lemma MOV_RM0_rule (pd:DWORD) (r1 r2:Reg) (v1 v2: DWORD) :
  |-- basic (r1 ~= v1 ** r2 ~= pd ** pd :-> v2)
            (MOV r1, [r2])
            (r1 ~= v2 ** r2 ~= pd ** pd :-> v2).
Proof. basic apply *. Qed.

Lemma MOV_RanyM0_rule (pd:DWORD) (r1 r2:Reg) (v2: DWORD) :
  |-- basic (r1? ** r2 ~= pd ** pd :-> v2)
            (MOV r1, [r2])
            (r1 ~= v2 ** r2 ~= pd ** pd :-> v2).
Proof. unhideReg r1 => old. basic apply *. Qed.

(** ** Register to memory *)
Lemma MOV_MR_rule (p: DWORD) (r1 r2: Reg) offset (v1 v2:DWORD) :
  |-- basic (r1~=p ** p +# offset :-> v1 ** r2~=v2)
            (MOV [r1 + offset], r2)
            (r1~=p ** p +# offset :-> v2 ** r2~=v2).
Proof. basic apply *. Qed.

(** ** Immediate to memory *)
Lemma MOV_MI_rule s (pd:DWORD) (r:Reg) offset (v w:VWORD s) :
  |-- basic (r ~= pd ** pd +# offset :-> v)
            (MOVOP _ (DstSrcMI _ (mkMemSpec (Some(r, None)) #offset) w))
            (r ~= pd ** pd +# offset :-> w).
Proof. basic apply *. Qed.

Lemma MOV_M0R_rule (pd:DWORD) (r1 r2:Reg) (v1 v2: DWORD) :
  |-- basic (r1 ~= pd ** pd :-> v1 ** r2 ~= v2)
            (MOV [r1], r2)
            (r1 ~= pd ** pd :-> v2 ** r2 ~= v2).
Proof. basic apply *. Qed.

Lemma MOV_IndR_rule (pd:DWORD) (r:Reg) (v1 v2: DWORD) :
  |-- basic (pd :-> v1 ** r ~= v2)
            (MOV [pd], r)
            (pd :-> v2 ** r ~= v2).
Proof. basic apply *. Qed.

Lemma MOV_MbR_rule (p: DWORD) (r1:Reg) (r2: BYTEReg) offset (v1:BYTE) (v2:BYTE) :
  |-- basic (r1 ~= p ** p +# offset :-> v1 ** r2 ~= v2)
            (MOV [r1 + offset], r2)
            (r1 ~= p ** p +# offset :-> v2 ** r2 ~= v2).
Proof. basic apply *. Qed.

Lemma MOV_RMb_rule (p: DWORD) (r1:Reg) (r2:BYTEReg) offset (v1:BYTE) (v2:BYTE) :
  |-- basic (r1 ~= p ** p +# offset :-> v1 ** r2 ~= v2)
            (MOV r2, [r1 + offset])
            (r1 ~= p ** p +# offset :-> v1 ** r2 ~= v1).
Proof. basic apply *. Qed.

Lemma MOV_MbI_rule (pd:DWORD) (r1:Reg) offset (v1 v2:BYTE) :
  |-- basic (r1 ~= pd ** pd +# offset :-> v1)
            (MOV BYTE [r1 + offset], v2)
            (r1 ~= pd ** pd +# offset :-> v2).
Proof. basic apply *. Qed.

author: nbenton