text:
(****************************************************************************)
(* Copyright (c) Facebook, Inc. and its affiliates.                         *)
(*                                                                          *)
(* Licensed under the Apache License, Version 2.0 (the "License");          *)
(* you may not use this file except in compliance with the License.         *)
(* You may obtain a copy of the License at                                  *)
(*                                                                          *)
(*     http://www.apache.org/licenses/LICENSE-2.0                           *)
(*                                                                          *)
(* Unless required by applicable law or agreed to in writing, software      *)
(* distributed under the License is distributed on an "AS IS" BASIS,        *)
(* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. *)
(* See the License for the specific language governing permissions and      *)
(* limitations under the License.                                           *)
(****************************************************************************)
From mathcomp.ssreflect
Require Import ssreflect ssrbool ssrnat eqtype ssrfun seq choice fintype path finset.
Require Import Eqdep.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Section SeqSubMissing.
Variables (T : choiceType) (s : seq T).
Local Notation sT := (seq_sub s).

Variable (D: pred T).

Lemma card_seq_sub : uniq s -> #|[set x:sT| D (val x)]| = size (filter D s).
Proof.
move=> Us; case: (pickP (fun x: sT => D(val x)))=> [x Px |P0].
- rewrite -(card_seq_sub (filter_uniq D Us)).
  move/valP: (x)=> Hx.
  have: (val x \in filter D s); first by rewrite mem_filter Px Hx.
  rewrite -(codom_val (seq_sub_subFinType (filter D s))).
  move/codomP=> [x0 Hxx0]; pose f := fun (x:sT) => insubd x0 (val x).
  rewrite -(@card_in_imset _ _ f); first apply eq_card.
  - move=> x1; rewrite inE; apply/idP; apply/imsetP.
    move/valP: (x1); rewrite mem_filter; move/andP=> [Dx1 Hx1].
    exists (insubd x (val x1)); last by rewrite /f /= insubdK; [rewrite valKd| rewrite Hx1 ].
    by rewrite /insubd (insubT _) inE /= Dx1.
  move=> y2 y1 Hy2 Hy1; rewrite in_set in Hy1; rewrite in_set in Hy2.
  rewrite /f /insubd (insubT _) /=; first by  rewrite mem_filter (valP y2) Hy2.
  rewrite (insubT _) /=; first by rewrite mem_filter (valP y1) Hy1.
  move=> Hyp1 Hyp2; case; apply val_inj.
rewrite cardsE; move/eq_card0: (P0)=>->; rewrite size_filter.
apply/eqP/negPn; rewrite eq_sym -lt0n -has_count.
rewrite negbT //; apply/hasP; move => [x Hx Dx].
move: Hx; rewrite -(codom_val (seq_sub_subFinType s))=> Hcd.
by move/codomP: Hcd=> [x0 Hxx0]; move: (P0 x0); rewrite -Hxx0 Dx.
Qed.

End SeqSubMissing.

From fcsl
Require Import pred prelude ordtype pcm finmap unionmap heap.
From LibraChain
Require Import SeqFacts Chains HashSign Blocks ConsensusState BlockTree BFTFacts.

Section Safety.
(* We require Hashes, Addresses, Signatures and PublicKeys to be numbers in *)
(* some fashion, i.e. to have an injective embedding in ints *)
Variable Hash : countType.

Variables (PublicKey: countType) (Signature: countType).
Variable Address: hashType PublicKey.

(* The Block Data (w/o signatures) *)
Notation BDataType := (BlockData Hash Signature Address Command NodeTime).

Variable hashB: BDataType -> Hash.
Hypothesis inj_hashB: injective hashB.

Variable verifB: Hash -> PublicKey -> Signature -> bool.

(* Block Type : block data with signatures *)
Notation BType := (BlockType inj_hashB verifB).
Notation QC := (QuorumCert Hash Signature (Phant Address)).

Canonical BDHType := Eval hnf in (Block_hashType inj_hashB).
Canonical BSType := Eval hnf in (Block_signType inj_hashB verifB).

Implicit Type b: BDataType.

Notation "# b" := (hashB b) (at level 20).

Parameter peers : seq Address.

(* f is the byzantine fraction (see below) *)
Variable f: nat.

(* boolean predicate for all signatures in a sequence to be valid *)
Definition all_valid (h: Hash) (s: seq (PublicKey * Signature)) :=
  all (fun ps => (@verify_op _ _ _ BSType h (fst ps) (snd ps))) s.

(* a valid qc only contains distinct and valid signatures *)
Definition qc_valid (qc: QC) :=
  all_valid (block_hash (qc_vote_data qc)) (qc_votes qc) && (uniq (qc_votes qc)).

(* a valid block is properly signed by its emitter *)
Definition source_valid (block: BType) :=
  let: (p, s) := (block_source block) in
       (@verify_op _ _ _ BSType (#block) p s).

Notation BlockStore := (BlockTree inj_hashB verifB).

(* Nodes have a public key, log of processed blocks and block store*)
Record NodeState := mkNode {
    public_key: PublicKey;
    block_log: seq BType;
}.

Definition node_state2components (ns: NodeState) :=
  let: mkNode pk bl := ns in (pk, bl).

Definition components2node_state (tuple: PublicKey * seq BType) :=
  let: (pk, bl) := tuple in mkNode pk bl.

Lemma can_ns_components: ssrfun.cancel node_state2components components2node_state.
Proof. by move => []. Qed.

(* There are a half-dozen wrong things that have turned wrong for me to do this by hands, TODO: *)
(* diagnose & fix*)
Canonical BlockTree_eqType := (union_map_eqType [ordType of Hash] [eqType of BType]).

Definition ns_eqMixin := CanEqMixin can_ns_components.
Canonical ns_eqType := EqType _ ns_eqMixin.

Definition ns_choiceMixin := CanChoiceMixin can_ns_components.
Canonical ns_choiceType := ChoiceType _ ns_choiceMixin.

Definition ns_countMixin := CanCountMixin can_ns_components.
Canonical ns_countType := CountType _ ns_countMixin.

Notation GenesisState := (genesis_state inj_hashB verifB ).

Definition addr_of(n: NodeState) := (hash_op Address (public_key n)).

Definition qc_keys(qc: QC) :=
  unzip1 (qc_votes qc).

Definition qc_addresses(qc: QC) :=
  map (hash_op Address) (qc_keys qc).

Variable validator_nodes: seq NodeState.
Hypothesis Huniq: uniq validator_nodes.
Hypothesis inj_keys: {in validator_nodes, injective public_key}.

Definition Validator:= seq_sub validator_nodes.

Definition node_keys :=
  map public_key validator_nodes.

Definition NodeKey := seq_sub node_keys.

Lemma mem_node_keys (v: Validator):
  (public_key (val v)) \in node_keys.
Proof.
rewrite /node_keys; apply/mapP; exists (val v)=> //.
by move/valP: (v).
Qed.

Definition to_pk (v: Validator): NodeKey :=
  Sub (public_key (val v)) (mem_node_keys v).

Lemma inj_to_pk : injective to_pk.
Proof.
move=> x1 x2; case; by move/(inj_keys (valP x1))/val_inj.
Qed.

Definition qc_relevant(qc: QC):=
  filter (fun pk => pk \in node_keys) (undup (qc_keys qc)).

(* There is a finite number of blocks at any given time *)

Definition all_blocks :=
  flatten [seq block_log n | n <- validator_nodes].

Definition BlockFinType := seq_sub all_blocks.

Section ValidBlocks.

Definition valid_pred (block: BType) :=
  source_valid block && qc_valid (qc_of block) && (size (qc_relevant (qc_of block)) == 2*f+1) && (qc_hash block != #block).

(* Valid blocks are the small subType which presents with enough valid *)
(* signatures *)
Record valid_block : Type := mkValid {
    block :> BlockFinType;
    _: valid_pred (val block);
}.

Canonical valid_block_subType := Eval hnf in [subType for block].
Definition valid_block_eqMixin := Eval hnf in [eqMixin of valid_block by <:].
Canonical valid_block_eqType := Eval hnf in EqType _ valid_block_eqMixin.
Definition valid_block_choiceMixin := [choiceMixin of valid_block by <:].
Canonical valid_block_choiceType := Eval hnf in ChoiceType valid_block valid_block_choiceMixin.
Definition valid_block_countMixin := [countMixin of valid_block by <:].
Canonical valid_block_countType := Eval hnf in CountType valid_block valid_block_countMixin.
Canonical valid_block_subCountType := Eval hnf in [subCountType of valid_block].
Definition valid_block_finMixin := [finMixin of valid_block by <:].
Canonical valid_block_finType := Eval hnf in FinType valid_block valid_block_finMixin.
Canonical valid_block_subFinType := Eval hnf in [subFinType of valid_block].

Implicit Type vb : valid_block.

Definition type_val (vb: valid_block) : BType :=
  ((val \o val) vb).
Coercion type_val: valid_block >-> BType.

Definition data_val (vb: valid_block) : BDataType :=
  ((val \o val) vb).
Coercion data_val: valid_block >-> BDataType.

Definition valid vb mkB : valid_block :=
  mkB (let: mkValid _ vbP := vb return (source_valid vb) && qc_valid (qc_of vb) && (size (qc_relevant (qc_of vb)) == 2*f+1) && (qc_hash vb != #vb) in vbP).

Lemma valid_blockE vb : valid (fun sP => @mkValid vb sP) = vb.
Proof. by case: vb. Qed.

Parameter GenesisBlock : valid_block.

(* node_in_votes captures the inclusion of this node in the block's signatures *)
Definition node_in_votes(n: NodeState): pred valid_block :=
  fun vb => addr_of n \in (qc_addresses (qc_of vb)).

Notation "'qc#' vb" := (qc_hash vb) (at level 40).

(* The parenthood relationship over valid blocks *)
Definition vb_parent :=
  [eta (parent hashB): rel valid_block].

(* The chaining relationship — parents with consecutive round — over valid blocks *)
Definition vb_direct_parent (vb1 vb2: valid_block) :=
  direct_parent vb1 vb2.

Definition voted_by_node(n: NodeState): seq BType :=
  [ seq b <- block_log n | ((block_data b) \in voted_in_processing GenesisState [seq block_data i | i <- block_log n]) && (valid_pred b)].

(* block_in_voting captures the inclusion of the valid block in the node's *)
(* voting log  *)
Definition block_in_voting(n: NodeState): pred valid_block :=
  fun (vb:valid_block) => has (fun b:BType => parent hashB b vb) (voted_by_node n).

(* This captures that the only blocks one can find this node's signatures are *)
(* those in its voting log => the node only votes according to the procedure *)
(* we describe in voted_by_node. *)
Definition honest : pred NodeState := fun n =>
  [set vb |node_in_votes n vb] \subset [set vb|block_in_voting n vb].

Hypothesis BFT:
  (#|[set x : Validator |honest (val x)]| >= (2*f).+1) &&
  (size validator_nodes == (3*f).+1).

(* the definition of node_in_votes through the injective hashes (addresses) of *)
(* public keys is the same as enumerating the public keys *)
Lemma nodes_in_votes_relevantE vb:
  [set v: Validator| node_in_votes (val v) vb] =
  [set v: Validator| (public_key (val v)) \in (qc_keys (qc_of vb))].
Proof.
apply eq_finset=> x/=.
rewrite /node_in_votes /qc_addresses /addr_of mem_map //.
by apply hash_inj.
Qed.

Lemma validators_in_votes vb:
  #|[set v: Validator| node_in_votes (val v) vb]| == (2*f).+1.
Proof.
rewrite -addn1.
move/valP/andP: (vb)=> [/andP[_ H] _]; move/eqP: H=><-; rewrite nodes_in_votes_relevantE.
rewrite (@card_seq_sub _ _ (fun (v:NodeState) => (public_key v) \in _) Huniq).
rewrite -(size_map public_key) -uniq_size_uniq.
- rewrite map_inj_in_uniq ?filter_uniq //.
  move=> x y; rewrite 2!mem_filter; move/andP=>[_ Hx]; move/andP=>[_ Hy].
  by apply (inj_keys Hx).
- by rewrite /qc_relevant filter_uniq // undup_uniq.
move=> x; rewrite /qc_relevant /node_keys mem_filter mem_undup.
by rewrite -filter_map mem_filter /= andbC.
Qed.

Lemma honest_in_one_block (vb: valid_block):
  exists (x: Validator), (node_in_votes (val x) vb) && honest (val x).
Proof.
move/card_S2f_gt: (validators_in_votes vb); move/(_ Huniq)=> Hcard.
move: (Hcard _ BFT).
move/(leq_ltn_trans (leq0n f)); rewrite card_gt0; move/set0Pn=>[x].
rewrite !inE; move/andP=> [Hn Hh]; by exists x; apply/andP.
Qed.

(* The intersection lemma implies a honest validator voted for any pair of blocks*)
Lemma honest_in_two_blocks (vb1 vb2: valid_block):
    exists (x:Validator), (node_in_votes (val x) vb1 && node_in_votes (val x) vb2 && honest (val x)).
Proof.
move: (validators_in_votes vb1) (validators_in_votes vb2)=> Hvb1 Hvb2.
move/andP: (conj Hvb1 Hvb2)=> H12; move: {Hvb1 Hvb2 H12}(intersectionP Huniq BFT H12).
move=>[x]; rewrite 4!inE; move/andP => [H12 Hhx]; move/andP: {H12}H12=>[H1 H2].
by exists x; rewrite Hhx H1 H2.
Qed.

(* That node has both blocks in its logs *)
Lemma honest_voted_two_blocks (vb1 vb2: valid_block):
  exists (n: Validator), (block_in_voting (val n) vb1) && (block_in_voting (val n) vb2 && honest(val n)).
Proof.
move: (honest_in_two_blocks vb1 vb2)=> [x]; move/andP=> [H12 Hh].
move/andP: H12=> [H1 H2]; exists x; rewrite Hh.
move/subsetP: (Hh); move/(_ vb1); rewrite inE H1 inE=> -> //.
by move/subsetP: Hh; move/(_ vb2); rewrite inE H2 inE=> -> //.
Qed.

(* This is the off-by one difference between most formalisms of LibraBFT and *)
(* the present Coq formalization. LibraBFT often speaks of confirmed / QC'ed blocks and *)
(* focuses on the blocks, treating the downward blocks which QC confirms them *)
(* implicitly. We can't afford to do this in Coq — since we chose to not have *)
(* an entire separate relation and type for "dangling" QCs — hence we have to *)
(* be very explicit with naming these confirming blocks. Hence note that here, *)
(* we express that if vb is in the vote log of n, its parent is voted for. *)
Lemma block_in_voting_processingP (n:NodeState) vb:
  (block_in_voting n vb) ->
  exists b, (parent hashB b vb) &&
    (b \in (voted_in_processing GenesisState [seq block_data i | i <- block_log n])).
Proof.
move/hasP=> [b Hvb Hhb]; exists b; rewrite Hhb andTb.
by move: Hvb; rewrite mem_filter; move/andP=> [/andP[-> Hval] Hlog].
Qed.

(* This is S2 in LibraBFT v2. The statement on state hashes is trivial *)
(* editing block_in_voting *)
Lemma valid_blocks_same_round_equal (vb1 vb2: valid_block):
  (qc_round vb1 == qc_round vb2) -> qc# vb1 == qc# vb2.
Proof.
move=> Hr.
move: (honest_voted_two_blocks vb1 vb2)=> [n]; move/andP=> [H1 /andP[H2 Hh]].
move/block_in_voting_processingP: H1=> [b1 /andP [Hb1 Hproc1]].
move/block_in_voting_processingP: H2=> [b2 /andP [Hb2 Hproc2]].
case H12: (b1 == b2).
- by move/andP: Hb1=>[/andP[/andP[/eqP[<-] _] _] _]; move/andP: Hb2=>[/andP[/andP[/eqP[<-] _] _] _]; move/eqP: H12=>->.
case/orP: (leq_total (round b1) (round b2)).
- move/(voted_in_processing_ltn (negbT H12) Hproc1 Hproc2); move/ltn_eqF.
  by move/andP: Hb1=>[/andP[/andP[_ /eqP[->]] _] _]; move/andP: Hb2=>[/andP[/andP[_ /eqP[->]] _] _]; rewrite Hr.
rewrite eq_sym in H12.
move/(voted_in_processing_ltn (negbT H12) Hproc2 Hproc1); move/ltn_eqF.
by move/andP: Hb1=>[/andP[/andP[_ /eqP[->]] _] _]; move/andP: Hb2=>[/andP[/andP[_ /eqP[->]] _] _]; rewrite eq_sym Hr.
Qed.

Lemma valid_qc_ancestor_is_parent (n: NodeState) (block: BType) vb:
  parent hashB block vb ->
  block_in_voting n vb ->
  (block_data block \in (voted_in_processing GenesisState [seq block_data i | i<- block_log n])).
Proof.
move=> Hpar.
move/block_in_voting_processingP=> [b0 /andP[/andP [/andP [/andP [Hb0 Hrd0] Hqc0] Hqcr0] Hproc0]].
move: (Hb0); move/andP: Hpar=> [/andP[/andP [/eqP[<-] _] _] _]; move/eqP/inj_hashB=> Hbb0.
by rewrite -Hbb0.
Qed.

(* Lemma S3 in LibraBFT v2, ported to v3 formalization *)
(* See comment of block_in_voting_processingP to understand why it takes us 4 *)
(* blocks to form a 3-chain *)
Lemma three_chain_higher (b0 b1 b2 c2 b c : valid_block):
  (path vb_direct_parent b0 [:: b1 ; b2 ]) && (vb_parent b2 c2) &&
  (vb_parent b c) ->
  (round b > round b2) ->
  (* a.k.a. previous_round b > round b0 in this presentation*)
  (qc_round b >= round b0).
Proof.
move/andP=> [/andP[Hpath Hpar23] Hparbc].
move: (honest_voted_two_blocks c2 c)=> [n /andP[Hvot3 /andP[Hvotc Hh]] Hqc].
move: (valid_qc_ancestor_is_parent Hparbc Hvotc) => Hbvot.
move: Hpath; rewrite /vb_direct_parent.
rewrite -cat1s cat_path; move/andP=>[Hb0b1]; rewrite /= andbT; move/andP=> [Hpar12 Hrd12].
move: Hb0b1; rewrite /= andbT; move/andP=> [Hpar01 Hrd01].
move: (valid_qc_ancestor_is_parent Hpar23 Hvot3) => H2vot.
move/andP: Hparbc=> [/andP[/andP[Hb /eqP[Hrd]] Hparent] Hparent_rd].
move/andP: (Hpar01)=> [/andP[/andP[H0 /eqP[Hrd0]] Hparent0] Hparent_rd0].
move/andP: (Hpar12)=> [/andP[/andP[H1 /eqP[Hrd1]] Hparent1] Hparent_rd1].
rewrite Hrd0 (eqP Hparent_rd1).
(* TODO : clean up type inference in this imbricated subtype*)
apply: (@voted_in_processing_subseq_qc_parent_rel _ _ _ _ _ _
        GenesisState [seq block_data i | i <- block_log (val n)]).
apply: voted_in_processing_both => //=.
- by apply/negPn=> H; move:Hqc; rewrite (eqP H) ltnn.
by rewrite ltnW.
Qed.

Lemma lt_wf_ind : forall (n : nat) (P : nat -> Prop),
  (forall n0 : nat, (forall m : nat, (m < n0) -> P m) -> P n0) ->
  P n.
Proof.
move=>n P H; apply: Wf_nat.lt_wf_ind=> [m mn].
by apply: (H m)=>[m0 m0m]; apply: mn; apply/ltP.
Qed.

Lemma logged_in_all_blocks (v: Validator) (b: BType):
  b \in block_log (val v) -> b \in all_blocks.
Proof.
move=> Hlog.
have H: (block_log (val v)) \in [seq block_log i | i <- validator_nodes].
- by apply/mapP; exists (val v)=> //; move/valP: (v).
by apply/flattenP; exists (block_log (val v)).
Qed.

Lemma valid_block_in_voting_processingP (v: Validator) vb:
  let n := val v in
  (block_in_voting n vb) ->
  exists b: valid_block, (vb_parent b vb) &&
    ((block_data b) \in (voted_in_processing GenesisState [seq block_data i | i <- block_log n])).
Proof.
rewrite /=; move/hasP=> [b Hvb Hhb].
move: Hvb; rewrite mem_filter; move/andP=> [/andP[Hvot Hval] Hlog].
move/logged_in_all_blocks: Hlog=>Hball; pose bb : BlockFinType := (Sub b Hball).
pose bv : valid_block := (Sub bb Hval).
exists bv; rewrite /= /vb_parent {1}/bv /parent.
by rewrite /type_val /comp !SubK -/(parent hashB b vb) Hhb andTb.
Qed.

(* Property S4 in LibraBFT v2, ported to v3 formalization *)

(* This includes a pretty strong variation in introducing d, the "lagging" *)
(* element in the blocks in comparison with the earlier three-chain.  'd' serves *)
(* exclusively to introduce a voted block carrying a QC for c, ensuring *)
(* qc_parent_round c < qc_round c, i.e.  qc_round b < round b, which is essential *)
(* to the use of the induction hypothesis. *)
(* We are therefore proving a weaker property than S4 — which is *)
(* incorrect as stated, though this technical error is of no consequence, since *)
(* the lemma yields the final theorem S5 anyway. *)
Lemma three_chain_linked (b0 b1 b2 c2 : valid_block):
  (path vb_direct_parent b0 [:: b1 ; b2 ]) && (vb_parent b2 c2) ->
  forall n: nat,
    (forall b c d: valid_block, (round b == n) && (path vb_parent b [:: c ; d]) && (round b >= round b0) ->
                           (exists bs: seq valid_block, (path vb_parent b0 bs) && (block_data (last b0 bs) == b))).
Proof.
move=>Hchain; elim/lt_wf_ind=> n IHn b c d; move/andP=>[/andP[Hn /andP[Hparbc /andP[Hparcd _]]] Hbb0].
case Hbb2: (round b > round b2).
- have Hqcb: (qc_round b >= round b0); first by apply: (@three_chain_higher b0 b1 b2 c2 b c); rewrite // Hparbc andbT Hchain.
  (* qc_round b <= round b — this is the only part that uses d *)
  have Hqc_cd: qc_parent_round c <= qc_round c.
  - move: (honest_in_one_block d)=> [nd /andP[Hvotd]].
    move/subsetP; move/(_ d); rewrite 2!inE; move/(_ Hvotd)=> Hvotingd.
    move: (valid_qc_ancestor_is_parent Hparcd Hvotingd).
    by move/voted_in_processing_exists=>[sb /andP[/andP[_ Hd] _]]; move: (voted_br_gt_qcr Hd).
  move: (Hparbc) Hqc_cd; rewrite {1}/vb_parent /parent; move/andP=>[/andP[/andP[_ /eqP[<-]] _] /eqP[<-]].
  (* set parb and prove round parb = qc_round b *)
  move: (honest_in_two_blocks b c)=> [node /andP[/andP[Hvotb Hvotc] Hhon]]; move/subsetP: (Hhon); move/(_ b).
  rewrite 2!inE; move/(_ Hvotb); move/valid_block_in_voting_processingP=> [parb /andP[Hparbb Hvotparb]].
  move: (Hparbb); rewrite {1}/vb_parent {1}/parent; move/andP=> [/andP[/andP[Hparb_h /eqP[Hrb]] _] _].
  rewrite -Hrb=> Hrd_parbb.
  (* establish parb != b & the prelude for voted_in_processing_ltn *)
  have Hrounds_parb_b : round parb < round b.
  - move/subsetP: Hhon; move/(_ c); rewrite 2!inE; move/(_ Hvotc).
    move/valid_block_in_voting_processingP=> [parc /andP[Hparc Hvotparc]].
    move: (Hparc) (Hparbc); rewrite {1 2}/vb_parent {1 2}/parent.
    move/andP=>[/andP[/andP[Hparc_h _] _] _]; move/andP=>[/andP[/andP[Hb_h _] _] _].
    move: Hb_h; rewrite -(eqP Hparc_h); move/eqP/inj_hashB=>Heqparcb; rewrite -Heqparcb in Hvotparc Hparc.
    apply: (voted_in_processing_ltn _ Hvotparb Hvotparc Hrd_parbb).
    move/valP: (b); move/andP=>[_]; rewrite -(eqP Hparb_h).
    by apply/contra=> HH; apply/eqP; congr hashB; rewrite (eqP HH) /=.
  rewrite (eqP Hn) in Hrounds_parb_b; move: (IHn (round parb) Hrounds_parb_b parb b c); rewrite eqxx andTb.
  rewrite -Hrb in Hqcb; rewrite Hqcb /= 2!andbT Hparbb Hparbc /=.
  move/(_ is_true_true)=> [bs Hbs]; exists (rcons bs b).
  rewrite rcons_path last_rcons eqxx andbT; move/andP: Hbs=>[->] /=.
  by case bs=>[|x xs] /=; rewrite /vb_parent; move/eqP=>->.
(* Prequel: unzip the vb_direct_parent assumption *)
move/andP: Hchain=> [Hchain Hb2c2]; have Hpar_chain: vb_parent b0 b1 && vb_parent b1 b2.
by move: Hchain; rewrite /= andbT /vb_direct_parent /direct_parent /vb_parent; move/andP=> [/andP[-> _] /andP[-> _]].
have Hrd_chain: (round b1 == (round b0).+1) && (round b2 == (round b1).+1).
by move: Hchain; rewrite /= andbT /vb_direct_parent /direct_parent; move/andP=> [/andP[_ ->] /andP[_ ->]].
(* Prequel : establish round b = qc_round c *)
move/andP: (Hparbc)=> [/andP[/andP[Hqch_c Hqc_c]  _ ] _].
move/negbT: Hbb2; rewrite -leqNgt leq_eqVlt; move/orP=>[Hbb2|Hbb2].
- move: Hb2c2; rewrite {1}/vb_parent {1}/parent; move/andP=>[/andP[/andP[Hqch_c2 Hqc_c2] _] _].
  move: Hbb2; rewrite (eqP Hqc_c2) (eqP Hqc_c); move/valid_blocks_same_round_equal.
  rewrite -(eqP Hqch_c) -(eqP Hqch_c2); move/eqP/inj_hashB=> Heq_bb2.
  by exists [:: b1; b2]; rewrite /= andbT Hpar_chain andTb eq_sym; apply/eqP.
move: Hbb2; move/andP: (Hrd_chain)=>[_ /eqP[->]]; rewrite ltnS leq_eqVlt; move/orP=> [Hbb1|Hbb1].
- move: Hbb1; rewrite (eqP Hqc_c); move/andP: (Hpar_chain)=>[_]; rewrite {1}/vb_parent {1}/parent.
  move/andP=> [/andP[/andP[Hqch_b1 /eqP[->]] _] _]; move/valid_blocks_same_round_equal.
  rewrite -(eqP Hqch_c) -(eqP Hqch_b1); move/eqP/inj_hashB=> Heq_bb1.
  by exists [:: b1]; rewrite /= Heq_bb1 eqxx 2!andbT; move/andP: Hpar_chain=> [-> _].
move: Hbb1; move/andP: Hrd_chain=> [/eqP[->] _]; rewrite ltnS=> Hbb1.
move: (eqn_leq (round b0) (round b)); rewrite {}Hbb0 {}Hbb1 andbT; move/idP.
move: Hpar_chain; rewrite andbC; move/andP=>[_]; rewrite {1}/vb_parent {1}/parent.
move/andP=> [/andP[/andP[Hqch_b0 /eqP[->]] _] _]; rewrite (eqP Hqc_c).
move/valid_blocks_same_round_equal; rewrite -(eqP Hqch_b0) -(eqP Hqch_c).
move/eqP/inj_hashB=> Hbb0.
by exists [::]=>/=; apply/eqP.
Qed.

Theorem safety (b0 b1 b2 c2: valid_block) (d0 d1 d2 e2: valid_block):
  (path vb_direct_parent b0 [:: b1 ; b2 ]) && (vb_parent b2 c2) ->
  (path vb_direct_parent d0 [:: d1 ; d2 ]) && (vb_parent d2 e2) ->
  (exists bs: seq valid_block, (path vb_parent b0 bs) && (block_data (last b0 bs) == d0)) \/
  (exists ds: seq valid_block, (path vb_parent d0 ds) && (block_data (last d0 ds) == b0)).
Proof.
wlog: b0 b1 b2 c2 d0 d1 d2 e2 / (round b0 <= round d0)=> H Hb0 Hd0.
- move/orP: (leq_total (round b0) (round d0))=>[H1|H1];
  [move: (H b0 b1 b2 c2 _ d1 d2 e2 H1 Hb0 Hd0) | move: (H d0 d1 d2 e2 _ b1 b2 c2 H1 Hd0 Hb0) ]; try by apply.
  by case; [right|left].
left; apply: (@three_chain_linked _ _ _ _ Hb0 (round d0) d0 d1 d2).
rewrite eq_refl andTb H andbT /= andbT; move/andP: Hd0=>[/andP[H1 /andP[H2 _]] _].
by rewrite /vb_parent; move/andP: H1=>[-> _]; move/andP: H2=>[-> _].
Qed.

End ValidBlocks.

End Safety.

author: novifinancial

repo: LibraChain


text:
Load LFindLoad.
From lfind Require Import LFind.
From QuickChick Require Import QuickChick.
From adtind Require Import goal33.

Derive Show for natural.

              Derive Arbitrary for natural.

              Instance Dec_Eq_natural : Dec_Eq natural.

              Proof. dec_eq. Qed.

Lemma conj23eqsynthconj2 : forall  (lv0 : natural) (lv1 : natural), (@eq natural (plus lv0 lv1) (plus Zero (plus lv1 lv0))).
Admitted.
QuickChick conj23eqsynthconj2.

author: yalhessi

repo: lemmaranker

save_path: github-repos/coq/yalhessi-lemmaranker


text:
Require Export XR_Rdiv.
Require Export XR_Rmult_lt_0_compat.
Require Export XR_Rinv_0_lt_compat.

Local Open Scope R_scope.

Lemma Rdiv_lt_0_compat : forall a b,
  R0 < a ->
  R0 < b ->
  R0 < a / b.
Proof.
  intros x y hx hy.
  unfold Rdiv.
  apply Rmult_lt_0_compat.
  { exact hx. }
  {
    apply Rinv_0_lt_compat.
    exact hy.
  }
Qed.

author: xavierdpt

repo: research

save_path: github-repos/coq/xavierdpt-research


text:
Require Import Relations.
Require Import FSets.
Require Import Arith.
Require Import Omega.

Set Keyed Unification.

Lemma Bool_elim_bool : forall (b:bool),b=true \/ b=false.
  destruct b;try tauto.
Qed.

Module OrderedPair (X:OrderedType) (Y:OrderedType) <: OrderedType with
Definition t := (X.t * Y.t)%type.
  Definition t := (X.t * Y.t)%type.

  Definition eq (xy1:t) (xy2:t) :=
    let (x1,y1) := xy1 in
      let (x2,y2) := xy2 in
        (X.eq x1 x2) /\ (Y.eq y1 y2).

  Definition lt (xy1:t) (xy2:t) :=
    let (x1,y1) := xy1 in
      let (x2,y2) := xy2 in
        (X.lt x1 x2) \/ ((X.eq x1 x2) /\ (Y.lt y1 y2)).

  Lemma eq_refl : forall (x:t),(eq x x).
    destruct x.
    unfold eq.
    split;[apply X.eq_refl | apply Y.eq_refl].
  Qed.

  Lemma eq_sym : forall (x y:t),(eq x y)->(eq y x).
    destruct x;destruct y;unfold eq;intro.
    elim H;clear H;intros.
    split;[apply X.eq_sym | apply Y.eq_sym];trivial.
  Qed.

  Lemma eq_trans : forall (x y z:t),(eq x y)->(eq y z)->(eq x z).
    unfold eq;destruct x;destruct y;destruct z;intros.
    elim H;clear H;intros.
    elim H0;clear H0;intros.
    split;[eapply X.eq_trans | eapply Y.eq_trans];eauto.
  Qed.

  Lemma lt_trans : forall (x y z:t),(lt x y)->(lt y z)->(lt x z).
    unfold lt;destruct x;destruct y;destruct z;intros.
    case H;clear H;intro.
    case H0;clear H0;intro.
    left.
    eapply X.lt_trans;eauto.
    elim H0;clear H0;intros.
    left.
    case (X.compare t0 t4);trivial;intros.
    generalize (X.eq_sym H0);intro.
    generalize (X.eq_trans e H2);intro.
    elim (X.lt_not_eq H H3).
    generalize (X.lt_trans l H);intro.
    generalize (X.eq_sym H0);intro.
    elim (X.lt_not_eq H2 H3).
    elim H;clear H;intros.
    case H0;clear H0;intro.
    left.
    case (X.compare t0 t4);trivial;intros.
    generalize (X.eq_sym H);intro.
    generalize (X.eq_trans H2 e);intro.
    elim (X.lt_not_eq H0 H3).
    generalize (X.lt_trans H0 l);intro.
    generalize (X.eq_sym H);intro.
    elim (X.lt_not_eq H2 H3).
    elim H0;clear H0;intros.
    right.
    split.
    eauto.
    eauto.
  Qed.

  Lemma lt_not_eq : forall (x y:t),(lt x y)->~(eq x y).
    unfold lt, eq;destruct x;destruct y;intro;intro.
    elim H0;clear H0;intros.
    case H.
    intro.
    apply (X.lt_not_eq H2 H0).
    intro.
    elim H2;clear H2;intros.
    apply (Y.lt_not_eq H3 H1).
  Qed.

  Definition compare : forall (x y:t),(Compare lt eq x y).
    destruct x;destruct y.
    case (X.compare t0 t2);intro.
    apply LT.
    left;trivial.
    case (Y.compare t1 t3);intro.
    apply LT.
    right.
    tauto.
    apply EQ.
    split;trivial.
    apply GT.
    right;auto.
    apply GT.
    left;trivial.
  Defined.

  Definition eq_dec : forall (x y: t), { eq x y } + { ~ eq x y}.
  Proof.
    intros [xa xb] [ya yb]; simpl.
    destruct (X.eq_dec xa ya).
    destruct (Y.eq_dec xb yb).
    + left; now split.
    + right. now intros [eqa eqb].
    + right. now intros [eqa eqb].
  Defined.

  Hint Immediate eq_sym.
  Hint Resolve eq_refl eq_trans lt_not_eq lt_trans.
End OrderedPair.

Module MessageSpi.
  Inductive message : Set :=
  | MNam : nat -> message.

  Definition t := message.

  Fixpoint message_lt (m n:message) {struct m} : Prop :=
    match (m,n) with
      | (MNam n1,MNam n2) => n1 < n2
    end.

  Module Ord <: OrderedType with Definition t := message with Definition eq :=
@eq message.
    Definition t := message.
    Definition eq := @eq message.
    Definition lt := message_lt.

    Lemma eq_refl : forall (x:t),eq x x.
      unfold eq;auto.
    Qed.

    Lemma eq_sym : forall (x y:t),(eq x y )->(eq y x).
      unfold eq;auto.
    Qed.

    Lemma eq_trans : forall (x y z:t),(eq x y)->(eq y z)->(eq x z).
      unfold eq;auto;intros;congruence.
    Qed.

    Lemma lt_trans : forall (x y z:t),(lt x y)->(lt y z)->(lt x z).
      unfold lt.
      induction x;destruct y;simpl;try tauto;destruct z;try tauto;intros.
      omega.
    Qed.

    Lemma lt_not_eq : forall (x y:t),(lt x y)->~(eq x y).
      unfold eq;unfold lt.
      induction x;destruct y;simpl;try tauto;intro;red;intro;try (discriminate
H0);injection H0;intros.
      elim (lt_irrefl n);try omega.
    Qed.

    Definition compare : forall (x y:t),(Compare lt eq x y).
      unfold lt, eq.
      induction x;destruct y;intros;try (apply LT;simpl;trivial;fail);try
(apply
GT;simpl;trivial;fail).
      case (lt_eq_lt_dec n n0);intros;try (case s;clear s;intros).
      apply LT;trivial.
      apply EQ;trivial.
      rewrite e;trivial.
      apply GT;trivial.
    Defined.

    Definition eq_dec : forall (x y: t), { eq x y } + { ~ eq x y}.
    Proof.
    intros [i] [j]. unfold eq.
    destruct (eq_nat_dec i j).
    + left. now f_equal.
    + right. intros meq; now inversion meq.
    Defined.

    Hint Immediate eq_sym.
    Hint Resolve eq_refl eq_trans lt_not_eq lt_trans.
  End Ord.

  Theorem eq_dec : forall (m n:message),{m=n}+{~(m=n)}.
    intros.
    case (Ord.compare m n);intro;[right | left | right];try (red;intro).
    elim (Ord.lt_not_eq m n);auto.
    rewrite e;auto.
    elim (Ord.lt_not_eq n m);auto.
  Defined.
End MessageSpi.

Module MessagePair := OrderedPair MessageSpi.Ord MessageSpi.Ord.

Module Type Hedge := FSetInterface.S with Module E := MessagePair.

Module A (H:Hedge).
  Definition hedge := H.t.

  Definition message_relation := relation MessageSpi.message.

  Definition relation_of_hedge (h:hedge) (m n:MessageSpi.message) := H.In (m,n)
h.

  Inductive hedge_synthesis_relation (h:message_relation) : message_relation :=
    | SynInc : forall (m n:MessageSpi.message),(h m
n)->(hedge_synthesis_relation h m n).

  Fixpoint hedge_in_synthesis (h:hedge) (m:MessageSpi.message)
(n:MessageSpi.message) {struct m} : bool :=
    if H.mem (m,n) h
      then true
      else false.

  Definition hedge_synthesis_spec (h:hedge) := hedge_synthesis_relation
(relation_of_hedge h).

  Lemma hedge_in_synthesis_impl_hedge_synthesis_spec : forall (h:hedge),forall
(m n:MessageSpi.message),(hedge_in_synthesis h m n)=true->(hedge_synthesis_spec
h m n).
    unfold hedge_synthesis_spec;unfold relation_of_hedge.
    induction m;simpl;intro.
    elim (Bool_elim_bool (H.mem (MessageSpi.MNam n,n0) h));intros.
    apply SynInc;apply H.mem_2;trivial.
    rewrite H in H0.  (* !! possible here !! *)
    discriminate H0.
  Qed.
End A.

Module B (H:Hedge).
  Definition hedge := H.t.

  Definition message_relation := relation MessageSpi.t.

  Definition relation_of_hedge (h:hedge) (m n:MessageSpi.t) := H.In (m,n) h.

  Inductive hedge_synthesis_relation (h:message_relation) : message_relation :=
    | SynInc : forall (m n:MessageSpi.t),(h m n)->(hedge_synthesis_relation h m
n).

  Fixpoint hedge_in_synthesis (h:hedge) (m:MessageSpi.t) (n:MessageSpi.t)
{struct m} : bool :=
    if H.mem (m,n) h
      then true
      else false.

  Definition hedge_synthesis_spec (h:hedge) := hedge_synthesis_relation
(relation_of_hedge h).

  Lemma hedge_in_synthesis_impl_hedge_synthesis_spec : forall (h:hedge),forall
(m n:MessageSpi.t),(hedge_in_synthesis h m n)=true->(hedge_synthesis_spec h m
n).
    unfold hedge_synthesis_spec;unfold relation_of_hedge.
    induction m;simpl;intro.
    elim (Bool_elim_bool (H.mem (MessageSpi.MNam n,n0) h));intros.
    apply SynInc;apply H.mem_2;trivial.
    rewrite H in H0. discriminate. (* !! impossible here !! *)
  Qed.
End B.

author: princeton-vl

repo: CoqGym

save_path: github-repos/coq/princeton-vl-CoqGym


Require Import Coq.omega.Omega.
Require Import Crypto.Compilers.SmartMap.

Set Implicit Arguments.
Set Asymmetric Patterns.

(** * Preliminaries: bounded and unbounded number types *)

Definition bound8 := 256.

Definition word8 := {n | n < bound8}.

Definition bound9 := 512.

Definition word9 := {n | n < bound9}.

(** * Expressions over unbounded words *)

Section unbounded.
  Variable var : Type.

  Inductive unbounded :=
  | Const : nat -> unbounded
  | Var : var -> unbounded
  | Plus : unbounded -> unbounded -> unbounded
  | LetIn : unbounded -> (var -> unbounded) -> unbounded.
End unbounded.

Arguments Const [var] _.

Definition Unbounded := forall var, unbounded var.

Fixpoint unboundedD (e : unbounded nat) : nat :=
  match e with
  | Const n => n
  | Var n => n
  | Plus e1 e2 => unboundedD e1 + unboundedD e2
  | LetIn e1 e2 => unboundedD (e2 (unboundedD e1))
  end.

Definition UnboundedD (E : Unbounded) : nat :=
  unboundedD (E _).

(** * Opt-in bounded types *)

Section bounded.
  Inductive type :=
  | Nat
  | Word8
  | Word9.

  Variable var : type -> Type.

  Inductive bounded : type -> Type :=
  | BConst : nat -> bounded Nat
  | BConst8 : word8 -> bounded Word8
  | BConst9 : word9 -> bounded Word9
  | BVar : forall t, var t -> bounded t
  | BPlus : bounded Nat -> bounded Nat -> bounded Nat
  | BPlus8 : bounded Word8 -> bounded Word8 -> bounded Word8
  | BPlus9 : bounded Word9 -> bounded Word9 -> bounded Word9
  | BLetIn : forall t1 t2, bounded t1 -> (var t1 -> bounded t2) -> bounded t2

  | Unbound : forall t, bounded t -> bounded Nat
  | Bound : forall t, bounded Nat -> bounded t.
End bounded.

Arguments BConst [var] _.
Arguments BConst8 [var] _.
Arguments BConst9 [var] _.
Arguments BVar [var t] _.
Arguments Unbound [var t] _.
Arguments Bound [var] _ _.

Definition Bounded t := forall var, bounded var t.

Definition typeD (t : type) : Type :=
  match t with
  | Nat => nat
  | Word8 => word8
  | Word9 => word9
  end.

Theorem O_lt_S : forall n, O < S n.
Proof.
  intros; omega.
Qed.

Definition plus8 (a b : word8) : word8 :=
  let n := proj1_sig a + proj1_sig b in
  match le_lt_dec bound8 n with
  | left _ => exist _ O (O_lt_S _)
  | right pf => exist _ n pf
  end.

Definition plus9 (a b : word9) : word9 :=
  let n := proj1_sig a + proj1_sig b in
  match le_lt_dec bound9 n with
  | left _ => exist _ O (O_lt_S _)
  | right pf => exist _ n pf
  end.

Infix "+8" := plus8 (at level 50).
Infix "+9" := plus9 (at level 50).

Definition unbound {t} : typeD t -> nat :=
  match t with
  | Nat => fun x => x
  | Word8 => fun x => proj1_sig x
  | Word9 => fun x => proj1_sig x
  end.

Definition bound {t} : nat -> typeD t :=
  match t return nat -> typeD t with
  | Nat => fun x => x
  | Word8 => fun x =>
               match le_lt_dec bound8 x with
               | left _ => exist _ O (O_lt_S _)
               | right pf => exist _ x pf
               end
  | Word9 => fun x =>
               match le_lt_dec bound9 x with
               | left _ => exist _ O (O_lt_S _)
               | right pf => exist _ x pf
               end
  end.

Fixpoint boundedD t (e : bounded typeD t) : typeD t :=
  match e with
  | BConst n => n
  | BConst8 n => n
  | BConst9 n => n
  | BVar _ n => n
  | BPlus e1 e2 => boundedD e1 + boundedD e2
  | BPlus8 e1 e2 => boundedD e1 +8 boundedD e2
  | BPlus9 e1 e2 => boundedD e1 +9 boundedD e2
  | BLetIn _ _ e1 e2 => boundedD (e2 (boundedD e1))
  | Unbound _ e1 => unbound (boundedD e1)
  | Bound _ e1 => bound (boundedD e1)
  end.

Definition BoundedD t (E : Bounded t) : typeD t :=
  boundedD (E _).

(** * Insertion of bounded types opportunistically *)

Definition fail {var} : nat * bounded var Nat := (0, BConst 0).

Fixpoint boundOf (eb : unbounded nat) : nat :=
  match eb with
  | Const n => n
  | Var n => n
  | Plus eb1 eb2 => boundOf eb1 + boundOf eb2
  | LetIn eb1 eb2 => boundOf (eb2 (boundOf eb1))
  end.

Fixpoint boundify {var} (eb : unbounded nat) (e : unbounded (var Nat)) : nat * bounded var Nat :=
  match e with
  | Const n => (n,
                match le_lt_dec bound8 n with
                | left _ =>
                  match le_lt_dec bound9 n with
                  | left _ => BConst n
                  | right pf => Unbound (BConst9 (exist _ n pf))
                  end
                | right pf => Unbound (BConst8 (exist _ n pf))
                end)
  | Var x =>
    match eb with
    | Var n => (n, BVar x)
    | _ => fail
    end
  | Plus e1 e2 =>
    match eb with
    | Plus eb1 eb2 =>
      let (n1, e1') := boundify eb1 e1 in
      let (n2, e2') := boundify eb2 e2 in
      (n1 + n2,
       if le_lt_dec bound8 (n1 + n2)
       then if le_lt_dec bound9 (n1 + n2)
            then BPlus e1' e2'
            else Unbound (BPlus9 (Bound _ e1') (Bound _ e2'))
       else Unbound (BPlus8 (Bound _ e1') (Bound _ e2')))
    | _ => fail
    end
  | LetIn e1 e2 =>
    match eb with
    | LetIn eb1 eb2 =>
      let (n1, e1') := boundify eb1 e1 in
      (boundOf (eb2 n1), BLetIn e1' (fun x => snd (boundify (eb2 n1) (e2 x))))
    | _ => fail
    end
  end.

Definition Boundify (E : Unbounded) : Bounded Nat :=
  fun _ => snd (boundify (E _) (E _)).

(** * Moving [Unbound] operators down from [LetIn]s to their use sites *)

Fixpoint movedown {var t} (e : bounded (bounded var) t) : bounded var t :=
  match e with
  | BConst n => BConst n
  | BConst8 n => BConst8 n
  | BConst9 n => BConst9 n
  | BVar _ e => e
  | BPlus e1 e2 => BPlus (movedown e1) (movedown e2)
  | BPlus8 e1 e2 => BPlus8 (movedown e1) (movedown e2)
  | BPlus9 e1 e2 => BPlus9 (movedown e1) (movedown e2)
  | BLetIn _ _ e1 e2 =>
    match movedown e1 in bounded _ t return (bounded _ t -> _) -> _ with
    | Unbound _ e1'' => fun e2_rec => BLetIn e1'' (fun x => e2_rec (Unbound (BVar x)))
    | e1' => fun e2_rec => BLetIn e1' (fun x => e2_rec (BVar x))
    end (fun x => movedown (e2 x))
  | Unbound _ e1 => Unbound (movedown e1)
  | Bound t e1 => Bound t (movedown e1)
  end.

Definition Movedown t (E : Bounded t) : Bounded t :=
  fun _ => movedown (E _).

(** * Canceling matching [Bound] and [Unbound] *)

Definition type_eq_dec : forall t1 t2 : type, {t1 = t2} + {t1 <> t2}.
Proof.
  decide equality.
Defined.

Fixpoint cancel {var t} (e : bounded var t) : bounded var t :=
  match e with
  | BConst n => BConst n
  | BConst8 n => BConst8 n
  | BConst9 n => BConst9 n
  | BVar _ x => BVar x
  | BPlus e1 e2 => BPlus (cancel e1) (cancel e2)
  | BPlus8 e1 e2 => BPlus8 (cancel e1) (cancel e2)
  | BPlus9 e1 e2 => BPlus9 (cancel e1) (cancel e2)
  | BLetIn _ _ e1 e2 => BLetIn (cancel e1) (fun x => cancel (e2 x))
  | Unbound _ e1 => Unbound (cancel e1)
  | Bound t e1 =>
    match cancel e1 with
    | Unbound t' e1' =>
      match type_eq_dec t' t with
      | left pf => match pf in _ = T return bounded _ T with
                   | eq_refl => e1'
                   end
      | right _ => Bound t (Unbound e1')
      end
    | e1' => Bound t e1'
    end
  end.

Definition Cancel t (E : Bounded t) : Bounded t :=
  fun _ => cancel (E _).

(** * Examples *)

Example ex1 : Unbounded := fun _ =>
  LetIn (Const 127) (fun a =>
  LetIn (Const 63) (fun b =>
  LetIn (Plus (Var a) (Var b)) (fun c =>
  Plus (Var c) (Var c)))).

Eval compute in (UnboundedD ex1).

Definition ex1b := Boundify ex1.
Eval compute in ex1b.

Definition ex1bm := Movedown (Boundify ex1).
Eval compute in ex1bm.

Definition ex1bmc := Cancel (Movedown (Boundify ex1)).
Eval compute in ex1bmc.


text:
Require Import Coq.Program.Basics.
Require Import Coq.Classes.Morphisms Coq.Setoids.Setoid.
Require Import Coq.Structures.Equalities.
Require Import Coq.Structures.Orders.
Require Import Crypto.Util.Structures.Equalities.Project.
Require Import Crypto.Util.Structures.Equalities.
Require Import Crypto.Util.Structures.Orders.
Require Import Crypto.Util.Tactics.SetoidSubst.
Require Import Crypto.Util.Tactics.BreakMatch.
Require Import Crypto.Util.Tactics.SplitInContext.
Require Import Crypto.Util.Tactics.DestructHead.

Local Set Implicit Arguments.

Module FlipHasLt (E : EqLt).
  Definition lt := flip E.lt.
End FlipHasLt.

Module FlipHasLe (E : EqLe).
  Definition le := flip E.le.
End FlipHasLe.

Module FlipIsStrOrder (E : StrOrder).
  Global Instance lt_strorder : StrictOrder (flip E.lt) | 10 := _.
  Global Instance lt_compat : Proper (E.eq==>E.eq==>iff) (flip E.lt) | 10 := _.
End FlipIsStrOrder.

Module FlipLeIsLtEq (E : EqLtLe') (Es : LeIsLtEq E) (Es' : IsEq E).
  Local Infix "<=" := (flip E.le).
  Local Infix "<" := (flip E.lt).
  Local Infix "==" := E.eq (at level 70).
  Lemma le_lteq : forall x y, x <= y <-> x < y \/ x == y.
  Proof.
    destruct Es'.eq_equiv.
    intros x y; cbv [flip]; rewrite Es.le_lteq; intuition eauto.
  Qed.
End FlipLeIsLtEq.

Module FlipHasCmp (E : Typ) (Ec : HasCmp E).
  Definition compare := flip Ec.compare.
End FlipHasCmp.

Module FlipCmpNotation (E : Typ) (Ec : HasCmp E).
  Module Import _FlipCmpNotation.
    Module C := FlipHasCmp E Ec.
  End _FlipCmpNotation.
  Include CmpNotation E C.
End FlipCmpNotation.

Module FlipCmpSpec (E : EqLt) (Ec : HasCompare E) (Ee : IsEq E).
  Local Infix "<" := (flip E.lt).
  Local Infix "==" := E.eq (at level 70).
  Lemma compare_spec : forall x y, CompareSpec (x == y) (x < y) (y < x) (flip Ec.compare x y).
  Proof.
    destruct Ee.eq_equiv.
    cbv [flip]; intros x y; destruct (Ec.compare_spec y x); constructor;
      eauto.
  Qed.
End FlipCmpSpec.

Module FlipLtIsTotal (E : EqLt) (Es : LtIsTotal E) (Ee : IsEq E).
  Local Infix "<" := (flip E.lt).
  Local Infix "==" := E.eq (at level 70).
  Lemma lt_total : forall x y, x < y \/ x == y \/ y < x.
  Proof.
    destruct Ee.eq_equiv.
    intros x y; destruct (Es.lt_total y x); destruct_head'_or; eauto.
  Qed.
End FlipLtIsTotal.

Module FlipHasLeb (E : Typ) (Es : HasLeb E).
  Definition leb := flip Es.leb.
End FlipHasLeb.

Module FlipHasLtb (E : Typ) (Es : HasLtb E).
  Definition ltb := flip Es.ltb.
End FlipHasLtb.

Module FlipLebNotation (E : Typ) (Es : HasLeb E).
  Module Import _FlipLebNotation.
    Module E' := FlipHasLeb E Es.
  End _FlipLebNotation.
  Include LebNotation E E'.
End FlipLebNotation.

Module FlipLtbNotation (E : Typ) (Es : HasLtb E).
  Module Import _FlipLtbNotation.
    Module E' := FlipHasLtb E Es.
  End _FlipLtbNotation.
  Include LtbNotation E E'.
End FlipLtbNotation.

Module FlipLebSpec (E : Typ) (Ee : HasEq E) (ELe : HasLe E) (ELeb : HasLeb E) (Es : LebSpec E ELe ELeb).
  Module Import _FlipLebSpec.
    Module E' := E <+ Ee <+ ELe <+ ELeb <+ Es.
    Module F := FlipHasLe E' <+ FlipHasLeb E' E'.
  End _FlipLebSpec.
  Lemma leb_le : forall x y, flip ELeb.leb x y = true <-> flip ELe.le x y.
  Proof.
    cbv [flip]; intros x y; apply Es.leb_le.
  Qed.
End FlipLebSpec.

Module FlipLtbSpec (E : Typ) (Ee : HasEq E) (ELt : HasLt E) (ELtb : HasLtb E) (Es : LtbSpec E ELt ELtb).
  Module Import _FlipLtbSpec.
    Module E' := E <+ Ee <+ ELt <+ ELtb <+ Es.
    Module F := FlipHasLt E' <+ FlipHasLtb E' E'.
  End _FlipLtbSpec.
  Lemma ltb_lt : forall x y, flip ELtb.ltb x y = true <-> flip ELt.lt x y.
  Proof.
    cbv [flip]; intros x y; apply Es.ltb_lt.
  Qed.
End FlipLtbSpec.

Local Coercion is_true : bool >-> Sortclass.

Module FlipLebIsTotal (E : EqLtLeBool) (ETotal : LebIsTotal E).
  Module Import _FlipLebIsTotal.
    Module F := FlipHasLeb E E.
  End _FlipLebIsTotal.
  Local Infix "<=?" := (flip E.leb) (at level 70).
  Lemma leb_total : forall x y, (x <=? y) = true \/ (y <=? x) = true.
  Proof.
    intros x y; destruct (ETotal.leb_total y x); eauto.
  Qed.
End FlipLebIsTotal.

Module FlipLebIsTransitive (E : LeBool) (ET : LebIsTransitive E).
  Lemma leb_trans : Transitive (flip E.leb).
  Proof.
    pose proof ET.leb_trans.
    cbv in *; eauto.
  Qed.
End FlipLebIsTransitive.

Module FlipLebIsTransitive_of_TotalOrderBool (E : TotalOrderBool).
  Module Import _FlipLebIsTransitive_of_TotalOrderBool.
    Module E' := E <+ TransitiveLeBool_of_TotalOrderBool.
  End _FlipLebIsTransitive_of_TotalOrderBool.
  Include FlipLebIsTransitive E' E'.
End FlipLebIsTransitive_of_TotalOrderBool.

Module Type FlipIsStrOrderBool (E : StrOrderBool).
  Module Import _FlipIsStrOrderBool.
    Module E' := E <+ IsEqbFacts.
  End _FlipIsStrOrderBool.
  Global Instance ltb_strorder : StrictOrder (flip E.ltb) | 10.
  Proof.
    cbv [flip]; destruct E'.ltb_strorder, E'.eqb_equiv; hnf in *.
    pose proof E'.ltb_compat.
    split; cbv in *; eauto.
  Qed.
  Global Instance ltb_compat : Proper (E.eqb==>E.eqb==>eq) (flip E.ltb) | 10.
  Proof.
    destruct E'.eqb_equiv; hnf in *.
    pose proof E'.ltb_compat.
    cbv in *; eauto.
  Qed.
End FlipIsStrOrderBool.

Module FlipLebIsLtbEqb (E : EqLtLeBool') (Es : LebIsLtbEqb E) (Ee : IsEqb E E).
  Lemma leb_ltbeqb : forall x y, (flip E.leb x y = (flip E.ltb x y || E.eqb x y))%bool.
  Proof.
    intros x y.
    pose proof ((_ : Symmetric E.eqb) x y).
    pose proof ((_ : Symmetric E.eqb) y x).
    cbv [flip]; intros; rewrite Es.leb_ltbeqb.
    cbv in *; break_innermost_match; eauto.
    do 2 destruct E.eqb; intuition congruence.
  Qed.
End FlipLebIsLtbEqb.

Module FlipUsualIsStrOrder (E : UsualStrOrder).
  Global Instance lt_strorder : StrictOrder (flip E.lt) | 10 := _.
  Global Instance lt_compat : Proper (eq==>eq==>iff) (flip E.lt) | 10 := _.
End FlipUsualIsStrOrder.

Module FlipUsualLeIsLtEq (E : UsualEqLtLe) (Es : LeIsLtEq E).
  Local Infix "<=" := (flip E.le).
  Local Infix "<" := (flip E.lt).
  Lemma le_lteq : forall x y, x <= y <-> x < y \/ x = y.
  Proof.
    cbv [flip]; intros; rewrite Es.le_lteq; intuition eauto.
  Qed.
End FlipUsualLeIsLtEq.

Module FlipUsualCmpSpec (E : UsualEqLt) (Ec : HasCompare E).
  Local Infix "<" := (flip E.lt).
  Lemma compare_spec : forall x y, CompareSpec (x = y) (x < y) (y < x) (flip Ec.compare x y).
  Proof.
    cbv [flip]; intros x y; destruct (Ec.compare_spec y x); constructor; eauto.
  Qed.
End FlipUsualCmpSpec.

Module FlipUsualLtIsTotal (E : UsualEqLt) (Es : LtIsTotal E).
  Local Infix "<" := (flip E.lt).
  Lemma lt_total : forall x y, x < y \/ x = y \/ y < x.
  Proof.
    cbv [flip]; intros x y; destruct (Es.lt_total y x); destruct_head'_or; eauto.
  Qed.
End FlipUsualLtIsTotal.

Module FlipEqLt (E : EqLt) <: EqLt := ProjectEq E <+ FlipHasLt E.
Module FlipEqLe (E : EqLe) <: EqLe := ProjectEq E <+ FlipHasLe E.
Module FlipEqLtLe (E : EqLtLe) <: EqLtLe := ProjectEq E <+ FlipHasLt E <+ FlipHasLe E.
Module FlipEqLt' (E : EqLt) <: EqLt' := ProjectEq E <+ FlipHasLt E <+ EqLtNotation.
Module FlipEqLe' (E : EqLe) <: EqLe' := ProjectEq E <+ FlipHasLe E <+ EqLeNotation.
Module FlipEqLtLe' (E : EqLtLe) <: EqLtLe' := ProjectEq E <+ FlipHasLt E <+ FlipHasLe E <+ EqLtLeNotation.
Module FlipStrOrder (E : StrOrder) <: StrOrder := ProjectEqualityType E <+ FlipHasLt E <+ FlipIsStrOrder E.
Module FlipStrOrder' (E : StrOrder) <: StrOrder' := FlipStrOrder E <+ EqLtNotation.
Module FlipHasCompare (E : EqLt) (Ec : HasCompare E) (Ee : IsEq E) := FlipHasCmp E Ec <+ FlipCmpSpec E Ec Ee.
Module FlipDecStrOrder (E : DecStrOrder) <: DecStrOrder := FlipStrOrder E <+ FlipHasCompare E E.
Module FlipDecStrOrder' (E : DecStrOrder) <: DecStrOrder' := FlipDecStrOrder E <+ EqLtNotation <+ CmpNotation.
Module FlipOrderedType (E : OrderedType) <: OrderedType := FlipDecStrOrder E <+ ProjectHasEqDec E.
Module FlipOrderedType' (E : OrderedType') <: OrderedType' := FlipOrderedType E <+ EqLtNotation <+ CmpNotation.
Module FlipOrderedTypeFull (E : OrderedTypeFull) <: OrderedTypeFull := FlipOrderedType E <+ FlipHasLe E <+ FlipLeIsLtEq E E E.
Module FlipOrderedTypeFull' (E : OrderedTypeFull') <: OrderedTypeFull' := FlipOrderedTypeFull E <+ EqLtLeNotation <+ CmpNotation.

Module FlipUsualEqLt (E : UsualEqLt) <: UsualEqLt := ProjectUsualEq E <+ FlipHasLt E.
Module FlipUsualEqLe (E : UsualEqLe) <: UsualEqLe := ProjectUsualEq E <+ FlipHasLe E.
Module FlipUsualEqLtLe (E : UsualEqLtLe) <: UsualEqLtLe := ProjectUsualEq E <+ FlipHasLt E <+ FlipHasLe E.

Module FlipUsualStrOrder (E : UsualStrOrder) <: UsualStrOrder := ProjectUsualEqualityType E <+ FlipHasLt E <+ FlipUsualIsStrOrder E.

Module FlipUsualHasCompare (E : UsualEqLt) (Ec : HasCompare E) := FlipHasCmp E Ec <+ FlipUsualCmpSpec E Ec.

Module FlipUsualDecStrOrder (E : UsualDecStrOrder) <: UsualDecStrOrder := FlipUsualStrOrder E <+ FlipUsualHasCompare E E.
Module FlipUsualOrderedType (E : UsualOrderedType) <: UsualOrderedType := FlipUsualDecStrOrder E <+ ProjectUsualHasEqDec E.
Module FlipUsualOrderedTypeFull (E : UsualOrderedTypeFull) <: UsualOrderedTypeFull := FlipUsualOrderedType E <+ FlipHasLe E <+ FlipUsualLeIsLtEq E E.

Module FlipUsualStrOrder' (E : UsualStrOrder) <: UsualStrOrder' := FlipUsualStrOrder E <+ LtNotation.
Module FlipUsualDecStrOrder' (E : UsualDecStrOrder) <: UsualDecStrOrder' := FlipUsualDecStrOrder E <+ LtNotation.
Module FlipUsualOrderedType' (E : UsualOrderedType) <: UsualOrderedType' := FlipUsualOrderedType E <+ LtNotation.
Module FlipUsualOrderedTypeFull' (E : UsualOrderedTypeFull) <: UsualOrderedTypeFull' := FlipUsualOrderedTypeFull E <+ LtLeNotation.

Module FlipTotalOrder (E : TotalOrder) <: TotalOrder := FlipStrOrder E <+ FlipHasLe E <+ FlipLeIsLtEq E E E <+ FlipLtIsTotal E E.
Module FlipUsualTotalOrder (E : UsualTotalOrder) <: UsualTotalOrder
:= FlipUsualStrOrder E <+ FlipHasLe E <+ FlipUsualLeIsLtEq E E <+ FlipUsualLtIsTotal E E.

Module FlipTotalOrder' (E : TotalOrder) <: TotalOrder' := FlipTotalOrder E <+ EqLtLeNotation.
Module FlipUsualTotalOrder' (E : UsualTotalOrder) <: UsualTotalOrder' := FlipUsualTotalOrder E <+ LtLeNotation.

Module FlipOrderedTypeOrig (E : MiniOrderedType) <: OrderedTypeOrig.
  Module Import _FlipOrderedTypeOrig.
    Module E' := OT_of_Orig E.
    Module F := FlipOrderedType E'.
  End _FlipOrderedTypeOrig.
  Include OT_of_New F.
End FlipOrderedTypeOrig.
Module FlipMiniOrderedType (E : MiniOrderedType) <: MiniOrderedType := FlipOrderedTypeOrig E.
Module FlipUsualOrderedTypeOrig (E : UsualMiniOrderedType) <: UsualOrderedTypeOrig.
  Module Import _FlipUsualOrderedTypeOrig.
    Module E' := UsualOT_of_UsualOrig E.
    Module F := FlipUsualOrderedType E'.
  End _FlipUsualOrderedTypeOrig.
  Include OT_of_New F.
End FlipUsualOrderedTypeOrig.
Module FlipUsualMiniOrderedType (E : UsualMiniOrderedType) <: UsualMiniOrderedType := FlipUsualOrderedTypeOrig E.

Module FlipLeBool (E : EqLeBool) <: LeBool := ProjectTyp E <+ FlipHasLeb E E.
Module FlipLtBool (E : EqLtBool) <: LtBool := ProjectTyp E <+ FlipHasLtb E E.
Module FlipLeBool' (E : EqLeBool) <: LeBool' := FlipLeBool E <+ LebNotation.
Module FlipLtBool' (E : EqLtBool) <: LtBool' := FlipLtBool E <+ LtbNotation.
Module FlipEqLeBool (E : EqLeBool) <: EqLeBool := ProjectTyp E <+ ProjectHasEqb E E <+ FlipHasLeb E E.
Module FlipEqLtBool (E : EqLtBool) <: EqLtBool := ProjectTyp E <+ ProjectHasEqb E E <+ FlipHasLtb E E.
Module FlipEqLeBool' (E : EqLeBool) <: EqLeBool' := FlipEqLeBool E <+ EqbNotation <+ LebNotation.
Module FlipEqLtBool' (E : EqLtBool) <: EqLtBool' := FlipEqLtBool E <+ EqbNotation <+ LtbNotation.
Module FlipEqLtLeBool (E : EqLtLeBool) <: EqLtLeBool := ProjectTyp E <+ ProjectHasEqb E E <+ FlipHasLtb E E <+ FlipHasLeb E E.
Module FlipEqLtLeBool' (E : EqLtLeBool) <: EqLtLeBool' := FlipEqLtLeBool E <+ EqbNotation <+ LtbNotation <+ LebNotation.

Module FlipTotalLeBool (E : TotalOrderBool) <: TotalLeBool := FlipLeBool E <+ FlipLebIsTotal E E.
Module FlipTotalLeBool' (E : TotalOrderBool) <: TotalLeBool' := FlipLeBool' E <+ FlipLebIsTotal E E.
Module FlipTotalEqLeBool (E : TotalOrderBool) <: TotalEqLeBool := FlipEqLeBool E <+ FlipLebIsTotal E E.
Module FlipTotalEqLeBool' (E : TotalOrderBool) <: TotalEqLeBool' := FlipEqLeBool' E <+ FlipLebIsTotal E E.
Module FlipTotalEqLtLeBool (E : TotalOrderBool) <: TotalEqLtLeBool := FlipEqLtLeBool E <+ FlipLebIsTotal E E.
Module FlipTotalEqLtLeBool' (E : TotalOrderBool) <: TotalEqLtLeBool' := FlipEqLtLeBool' E <+ FlipLebIsTotal E E.

Module FlipTotalTransitiveLeBool (E : TotalOrderBool) <: TotalTransitiveLeBool := FlipTotalLeBool E <+ FlipLebIsTransitive_of_TotalOrderBool E.
Module FlipTotalTransitiveLeBool' (E : TotalOrderBool) <: TotalTransitiveLeBool' := FlipTotalLeBool' E <+ FlipLebIsTransitive_of_TotalOrderBool E.
Module FlipTotalTransitiveEqLeBool (E : TotalOrderBool) <: TotalTransitiveEqLeBool := FlipTotalEqLeBool E <+ FlipLebIsTransitive_of_TotalOrderBool E.
Module FlipTotalTransitiveEqLeBool' (E : TotalOrderBool) <: TotalTransitiveEqLeBool' := FlipTotalEqLeBool' E <+ FlipLebIsTransitive_of_TotalOrderBool E.
Module FlipTotalTransitiveEqLtLeBool (E : TotalOrderBool) <: TotalTransitiveEqLtLeBool := FlipTotalEqLtLeBool E <+ FlipLebIsTransitive_of_TotalOrderBool E.
Module FlipTotalTransitiveEqLtLeBool' (E : TotalOrderBool) <: TotalTransitiveEqLtLeBool' := FlipTotalEqLtLeBool' E <+ FlipLebIsTransitive_of_TotalOrderBool E.

Module FlipStrOrderBool (E : StrOrderBool) <: StrOrderBool := ProjectEqbType E <+ FlipHasLtb E E <+ FlipIsStrOrderBool E.
Module FlipStrOrderBool' (E : StrOrderBool) <: StrOrderBool' := FlipStrOrderBool E <+ EqLtBoolNotation.

Module FlipTotalOrderBool (E : TotalOrderBool) <: TotalOrderBool := FlipStrOrderBool E <+ FlipHasLeb E E <+ FlipLebIsLtbEqb E E <+ FlipLebIsTotal E E.
Module FlipTotalOrderBool' (E : TotalOrderBool) <: TotalOrderBool' := FlipTotalOrderBool E <+ EqLtLeBoolNotation.

Module FlipHasBoolOrdFuns (E : Typ) (F : HasBoolOrdFuns E) := ProjectHasEqb E F <+ FlipHasLtb E F <+ FlipHasLeb E F.

Module FlipHasBoolOrdFuns' (E : Typ) (F : HasBoolOrdFuns E) := FlipHasBoolOrdFuns E F <+ EqbNotation E F <+ FlipLtbNotation E F <+ FlipLebNotation E F.

Module FlipBoolOrdSpecs (O : EqLtLe) (F : HasBoolOrdFuns O) (S : BoolOrdSpecs O F) := ProjectEqbSpec O O F S <+ FlipLtbSpec O O O F S <+ FlipLebSpec O O O F S.

Module FlipOrderFunctions (O : EqLtLe) (F : OrderFunctions O) (Oe : IsEq O) := FlipHasCompare O F Oe <+ FlipHasBoolOrdFuns O F <+ FlipBoolOrdSpecs O F F.

Module FlipOrderFunctions' (O : EqLtLe) (F : OrderFunctions O) (Oe : IsEq O) := FlipHasCompare O F Oe <+ FlipCmpNotation O F <+ FlipHasBoolOrdFuns' O F <+ FlipBoolOrdSpecs O F F.

author: mit-plv

repo: fiat-crypto

save_path: github-repos/coq/mit-plv-fiat-crypto


text:
(** SSReflect/Mathcomp の数学的構造 *)

Require Import List.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

(* Set Printing All. *)               (* コアーションを省かずに表示する。 *)

Definition negb (b : bool) := if b then false else true.
Definition pred := fun T : Type => T -> bool.
Definition rel := fun T : Type => T -> pred T.

Definition is_true (x : bool) : Prop := x = true.
Coercion is_true : bool >-> Sortclass.

Definition isSome (T : Type) (u : option T) :=
  match u return bool with
  | Some _ => true
  | None => false
  end.
Coercion isSome : option >-> bool.

Definition nat_of_bool (b : bool) := if b then 1 else 0.
Coercion nat_of_bool : bool >-> nat.

Fixpoint count (T : Type) (a : T -> bool) (s : list T) : nat :=
  match s with
  | nil => 0
  | (x :: s') => a x + count a s'           (* nat_of_bool *)
  end.

Inductive reflect (P : Prop) : bool -> Prop :=
| ReflectT :   P -> reflect P true
| ReflectF : ~ P -> reflect P false.

Definition eqfun (A B : Type) (f g : B -> A) := forall x : B, f x = g x.
Notation "f1 =1 f2" := (eqfun f1 f2) (at level 70, no associativity).

Definition pcancel (rT aT : Type) (f : aT -> rT) (g : rT -> option aT) :=
  forall x : aT, g (f x) = Some x.

(*
Section Relations.
  Variable S T R : Type.

  Definition associative (op : S -> S -> S) :=
    forall (x y z : S), op x (op y z) = op (op x y) z.
  Definition commutative (op : S -> S -> T) :=
    forall (x y : S), op x y = op y x.
  Definition left_id (e : S) (op : S -> T -> T) :=
    forall (x : T), op e x = x.
  Definition right_id (e : S) (op : T -> S -> T) :=
    forall (x : T), op x e = x.
  Definition left_inverse (e : R) (inv : T -> S) (op : S -> T -> R) :=
    forall (x : T), op (inv x) x = e.
  Definition left_distributive (op : S -> T -> S) (add : S -> S -> S) :=
    forall (x y : S) (z : T), op (add x y) z = add (op x z) (op y z).
  Definition right_distributive (op : S -> T -> T) (add : T -> T -> T) :=
    forall (x : S) (y z : T), op x (add y z) = add (op x y) (op x z).
End Relations.
*)

(** eqType *)
Module Equality.

  Record mixin_of (T : Type) :=
    Mixin {
        op : rel T;
        ax : forall x y : T, reflect (x = y) (op x y);
      }.

  Structure type :=
    Pack {
        sort :> Type;
        mixin : mixin_of sort;
      }.
End Equality.

Coercion Equality.sort : Equality.type >-> Sortclass.
Notation EqMixin := Equality.Mixin.
Notation eqType := Equality.type.
Notation EqType := Equality.Pack.

Definition eq_op {T : eqType} := Equality.op (Equality.mixin T).
Check @eq_op : forall T : eqType, rel (Equality.sort T).
Check @eq_op : forall T : eqType, rel T.
Notation "x == y" := (eq_op x y) (at level 70, no associativity).
Notation "x != y" := (negb (@eq_op _ x y)) (at level 70, no associativity).

(** ChoiceType 可算選択公理 *)
Module Choice.

  Record mixin_of (T : Type) :=
    Mixin {
        find : pred T -> nat -> option T;
        correct : forall P n x, find P n = Some x -> P x;
        complete : forall P : pred T, (exists x, P x) -> exists n, find P n; (* isSome *)
        extension : forall P Q : pred T, P =1 Q -> find P =1 find Q;
      }.

  Record class_of (T : Type) :=
    Class {
        base :> Equality.mixin_of T;
        mixin : mixin_of T;
      }.

  Structure type :=
    Pack {
        sort :> Type;
        class : class_of sort;
      }.

  Coercion eqType (cT : type) := EqType (base (class cT)).
End Choice.

Coercion Choice.base : Choice.class_of >-> Equality.mixin_of.
Coercion Choice.mixin : Choice.class_of >-> Choice.mixin_of.
Coercion Choice.sort : Choice.type >-> Sortclass.
Notation ChoiceMixin := Choice.Mixin.
Notation ChoiceClass := Choice.Class.
Notation choiceType := Choice.type.
Notation ChoiceType := Choice.Pack.
Canonical Structure Choice.eqType.

(** CountType *)
Module Countable.

  Record mixin_of (T : Type) :=
    Mixin {
        pickle : T -> nat;
        unpickle : nat -> option T;
        pickleK : pcancel pickle unpickle;
      }.

  Record class_of (T : Type) :=
    Class {
        base :> Choice.class_of T;
        mixin : mixin_of T;
      }.

  Structure type :=
    Pack {
        sort :> Type;
        class : class_of sort;
      }.

  Coercion eqType (cT : type) := EqType (base (class cT)).
  Coercion choiceType (cT : type) := ChoiceType (base (class cT)).
End Countable.

Coercion Countable.base : Countable.class_of >-> Choice.class_of.
Coercion Countable.mixin : Countable.class_of >-> Countable.mixin_of.
Coercion Countable.sort : Countable.type >-> Sortclass.
Notation CountMixin := Countable.Mixin.
Notation CountClass := Countable.Class.
Notation countType := Countable.type.
Notation CountType := Countable.Pack.
Canonical Structure Countable.eqType.
Canonical Structure Countable.choiceType.

(** finType *)
Module Finite.

  (* T : Equality.sort T *)
  Definition count_mem (T : eqType) (x : T) (e : list T) :=
    count (fun y => y == x) e.

  Definition axiom (T : eqType) (e : list T) :=
    forall x : T, (count_mem x) e = 1.

  Record mixin_of (T : eqType) :=
    Mixin {
        mixin_base : Countable.mixin_of T;
        mixin_enum : list T;
        ax : axiom mixin_enum
      }.

  Record class_of (T : eqType) :=
    Class {
        base :> Countable.class_of T;
        mixin : mixin_of T
      }.

  Structure type :=
    Pack {
        sort :> eqType;
        class : class_of sort
      }.

  Coercion eqType (cT : type) := EqType (base (class cT)).
  Coercion choiceType (cT : type) := ChoiceType (base (class cT)).
  Coercion countType (cT : type) := CountType (base (class cT)).
End Finite.

Coercion Finite.base : Finite.class_of >-> Countable.class_of.
Coercion Finite.mixin : Finite.class_of >-> Finite.mixin_of.
Coercion Finite.sort : Finite.type >-> eqType. (* Sortclass *)
Notation FinMixin := Finite.Mixin.
Notation FinClass := Finite.Class.
Notation finType := Finite.type.
Notation FinType := Finite.Pack.
Canonical Structure Finite.eqType.
Canonical Structure Finite.choiceType.
Canonical Structure Finite.countType.

(** GRing *)
(* Module GRing. *)

  Delimit Scope ring_scope with R.
  Open Scope ring_scope.

  (** Zmodule Z加群 *)
  Module Zmodule.

    Record mixin_of (V : Type) :=
      Mixin {
          zero : V;
          opp : V -> V;
          add : V -> V -> V;
          (* associative add *)
          ax1 : forall (x y z : V), add x (add y z) = add (add x y) z;
          (* commutative add *)
          ax2 : forall (x y : V), add x y = add y x;
          (* left_id zero add *)
          ax3 : forall (x : V), add zero x = x;
          (* left_inverse zero opp add *)
          ax4 : forall (x : V), add (opp x) x = zero;
        }.

    Record class_of (T : Type) :=
      Class {
          base : Choice.class_of T;
          mixin : mixin_of T
        }.

    Structure type :=
      Pack {
          sort :> Type;
          class : class_of sort;
          _ : Type;
        }.

    (* Pack の class メンバ関数とおなじなので、使わない。 *)
    Definition class' (cT : type) :=
      match cT as cT' return (class_of (sort cT')) with
      | @Pack sort class _ => class
      end.
    (* Mathcomp の場合： *)
    (* Definition class' := let: Pack s c as cT' := cT return class_of cT' in c. *)

    (*
    Coercion eqType (cT : type) :=
      @Equality.Pack (sort cT)
                     (@Choice.base (xT cT)
                                   (@base (xT cT) (class cT : class_of (xT cT)))).
     *)
    Coercion eqType (cT : type) := EqType (base (class cT)).
    Coercion choiceType (cT : type) := ChoiceType (base (class cT)).
  End Zmodule.

  Coercion Zmodule.base : Zmodule.class_of >-> Choice.class_of.
  Coercion Zmodule.mixin : Zmodule.class_of >-> Zmodule.mixin_of.
  Coercion Zmodule.sort : Zmodule.type >-> Sortclass.
  Notation ZmodMixin := Zmodule.Mixin.
  Notation ZmodClass := Zmodule.Class.
  Notation zmodType := Zmodule.type.
  Notation ZmodType := Zmodule.Pack.
  (* zmodType に対して、== と != を使えるようにする。 *)
  Canonical Structure Zmodule.eqType.       (* one != 0 のため。 *)
  Canonical Structure Zmodule.choiceType.

  (* zero などの引数に、コアーション Zmodule.mixin が機能する。 *)
  (* Zmodule.zero (Zmodule.mixin (Zmodule.class V)) *)
  Definition zero V := Zmodule.zero (Zmodule.class V).
  Definition opp V := Zmodule.opp (Zmodule.class V).
  Definition add V := Zmodule.add (Zmodule.class V).

  Local Notation "0" := (zero _) : ring_scope.
  Local Notation "-%R" := (@opp _) : ring_scope.
  Local Notation "- x" := (opp x) : ring_scope.
  Local Notation "+%R" := (@add _) : ring_scope.
  Local Notation "x + y" := (add x y) : ring_scope.
  Local Notation "x - y" := (x + - y) : ring_scope.

  (** Ring *)
  Module Ring.

    Record mixin_of (R : zmodType) :=
      Mixin {
          one : R;
          mul : R -> R -> R;
          (* associative mul *)
          ax1 : forall (x y z : R), mul x (mul y z) = mul (mul x y) z;
          (* left_id one mul *)
          ax2 : forall (x : R), mul one x = x;
          (* right_id one mul *)
          ax3 : forall (x : R), mul x one = x;
          (* left_distributive mul +%R *)
          ax4 : forall (x y : R) (z : R), mul (x + y) z = (mul x z) + (mul y z);
          (* right_distributive mul +%R *)
          ax5 : forall (x : R) (y z : R), mul x (y + z) = (mul x y) + (mul x z);
          ax6 : one != 0;
        }.

    Record class_of (R : Type) :=
      Class {
          base : Zmodule.class_of R;
          mixin : mixin_of (Zmodule.Pack base R);
        }.

    Structure type :=
      Pack {
          sort :> Type;
          class : class_of sort;
          _ : Type;
        }.

    Coercion eqType (cT : type) := EqType (base (class cT)).
    Coercion choiceType (cT : type) := ChoiceType (base (class cT)).
    Coercion zmodType (cT : type) := ZmodType (base (class cT)) cT. (* 3引数 *)
  End Ring.

  Coercion Ring.base : Ring.class_of >-> Zmodule.class_of.
  Coercion Ring.mixin : Ring.class_of >-> Ring.mixin_of.
  Coercion Ring.sort : Ring.type >-> Sortclass.
  Notation ringType := Ring.type.
  Notation RingType := Ring.Pack.
  Canonical Structure Ring.eqType.
  Canonical Structure Ring.choiceType.
  Canonical Structure Ring.zmodType.

(* End GRing. *)

(** ****** *)
(** sample *)
(** ****** *)

Require Import Bool.

(** eqType *)
Fail Check true == true.
Fail Check true != false.

(* Bool のなかにも、reflect があるため。 *)
Lemma eqb_spec : forall b1 b2, Top.reflect (b1 = b2) (eqb b1 b2).
Proof.
  intros b1 b2.
  destruct b1, b2; now constructor.
Qed.

Definition bool_eqMixin := EqMixin eqb_spec.
Canonical Structure bool_eqType := EqType bool_eqMixin.

Check bool_eqType : eqType.
Check true == true.
Check true != false.

(** choiceType *)

Definition choose (P : pred bool) (n : nat) :=
  match n with
  | 0 => Some false
  | 1 => Some true
  | _ => None
  end.

Lemma chooseP (P : pred bool) n x : choose P n = Some x -> P x.
Proof.
  intro H.
Admitted.

Lemma choose_id (P : pred bool) :
  (exists x, P x) -> exists n, choose P n. (* isSome *)
Proof.
Admitted.

Lemma eq_choose P Q : P =1 Q -> choose P =1 choose Q.
Proof.
  easy.
Qed.

Definition bool_choiceMixin := ChoiceMixin chooseP choose_id eq_choose.
Canonical Structure bool_choiceClass := ChoiceClass bool_eqMixin bool_choiceMixin.
Canonical Structure bool_choiceType := ChoiceType bool_choiceClass.

Check bool_choiceType : choiceType.

(** countType *)

Definition bool_pickle : bool -> nat := nat_of_bool.

Definition bool_unpickle : nat -> option bool :=
  fun n => match n with
           | 0 => Some false
           | 1 => Some true
           | _ => None
           end.

Lemma bool_pickleK : pcancel bool_pickle bool_unpickle.
Proof.
  intros b.
  now destruct b.
Qed.

Definition bool_countMixin := CountMixin bool_pickleK.
Canonical Structure bool_countClass := CountClass bool_choiceClass bool_countMixin.
Canonical Structure bool_countType := CountType bool_countClass.

Check bool_countType : countType.

(** finType *)

Definition bool_fin_enum := false :: true :: nil.

Lemma bool_fin_ax (x : bool) : (Finite.count_mem x) bool_fin_enum = 1.
Proof.
  unfold Finite.count_mem, bool_fin_enum.
  now destruct x.
Qed.

Definition bool_finMixin := FinMixin bool_countMixin bool_fin_ax.
Canonical Structure bool_finClass := FinClass bool_countClass bool_finMixin.
Canonical Structure bool_finType := FinType bool_finClass.

Check bool_finType : finType.

(* END *)

author: suharahiromichi

repo: coq

save_path: github-repos/coq/suharahiromichi-coq


text:
Require Import Coq.ZArith.ZArith.
Require Import Coq.NArith.NArith.
Require Import Coq.Strings.String.
Require Import Coq.Lists.List.
Require Import Coq.Classes.Morphisms.
Require Import Coq.Bool.Bool.
Require Import Crypto.Util.Option.
Require Import Crypto.Util.Bool.
Require Import Crypto.Util.Bool.Reflect.
Require Import Crypto.Util.ListUtil.
Require Import Crypto.Util.Tactics.DestructHead.
Require Import Crypto.Util.Notations.
Require Import Crypto.Assembly.Syntax.

Delimit Scope REG_scope with REG.
Bind Scope REG_scope with REG.

Infix "=?" := REG_beq : REG_scope.

Global Instance REG_beq_spec : reflect_rel (@eq REG) REG_beq | 10
  := reflect_of_beq internal_REG_dec_bl internal_REG_dec_lb.
Definition REG_beq_eq x y : (x =? y)%REG = true <-> x = y := conj (@internal_REG_dec_bl _ _) (@internal_REG_dec_lb _ _).
Lemma REG_beq_neq x y : (x =? y)%REG = false <-> x <> y.
Proof. rewrite <- REG_beq_eq; destruct (x =? y)%REG; intuition congruence. Qed.
Global Instance REG_beq_compat : Proper (eq ==> eq ==> eq) REG_beq | 10.
Proof. repeat intro; subst; reflexivity. Qed.

Definition CONST_beq : CONST -> CONST -> bool := Z.eqb.
Definition CONST_dec_bl (x y : CONST) : CONST_beq x y = true -> x = y := proj1 (Z.eqb_eq x y).
Definition CONST_dec_lb (x y : CONST) : x = y -> CONST_beq x y = true := proj2 (Z.eqb_eq x y).
Definition CONST_eq_dec (x y : CONST) : {x = y} + {x <> y} := Z.eq_dec x y.

Delimit Scope CONST_scope with CONST.
Bind Scope CONST_scope with CONST.

Infix "=?" := CONST_beq : CONST_scope.

Global Instance CONST_beq_spec : reflect_rel (@eq CONST) CONST_beq | 10
  := reflect_of_beq CONST_dec_bl CONST_dec_lb.
Definition CONST_beq_eq x y : (x =? y)%CONST = true <-> x = y := conj (@CONST_dec_bl _ _) (@CONST_dec_lb _ _).
Lemma CONST_beq_neq x y : (x =? y)%CONST = false <-> x <> y.
Proof. rewrite <- CONST_beq_eq; destruct (x =? y)%CONST; intuition congruence. Qed.
Global Instance CONST_beq_compat : Proper (eq ==> eq ==> eq) CONST_beq | 10.
Proof. repeat intro; subst; reflexivity. Qed.

Delimit Scope MEM_scope with MEM.
Bind Scope MEM_scope with MEM.

Definition MEM_beq (x y : MEM) : bool
  := ((Bool.eqb x.(mem_is_byte) y.(mem_is_byte))
      && (x.(mem_reg) =? y.(mem_reg))%REG
      && (option_beq REG_beq x.(mem_extra_reg) y.(mem_extra_reg))
      && (option_beq Z.eqb x.(mem_offset) y.(mem_offset)))%bool.
Global Arguments MEM_beq !_ !_ / .

Infix "=?" := MEM_beq : MEM_scope.

Local Ltac t_dec :=
  lazymatch goal with
  | [ |- ?beq ?x ?y = true -> ?x = ?y ]
    => is_var x; is_var y; destruct x, y; cbv [beq]
  | [ |- ?x = ?y -> ?beq ?x ?y = true ]
    => is_var x; is_var y; destruct x; cbv [beq]; intros; subst
  end;
  simpl;
  rewrite ?Bool.andb_true_iff; intros; destruct_head'_and;
  repeat apply conj; try reflexivity;
  reflect_hyps; subst;
  try solve [ reflexivity
            | exfalso; assumption
            | apply unreflect_bool; reflexivity ].

Lemma MEM_dec_bl (x y : MEM) : MEM_beq x y = true -> x = y.
Proof. t_dec. Qed.
Lemma MEM_dec_lb (x y : MEM) : x = y -> MEM_beq x y = true.
Proof. t_dec. Qed.
Definition MEM_eq_dec (x y : MEM) : {x = y} + {x <> y}
  := (if (x =? y)%MEM as b return (x =? y)%MEM = b -> _
      then fun pf => left (@MEM_dec_bl _ _ pf)
      else fun pf => right (fun pf' => diff_false_true (eq_trans (eq_sym pf) (@MEM_dec_lb _ _ pf'))))
       eq_refl.

Global Instance MEM_beq_spec : reflect_rel (@eq MEM) MEM_beq | 10
  := reflect_of_beq MEM_dec_bl MEM_dec_lb.
Definition MEM_beq_eq x y : (x =? y)%MEM = true <-> x = y := conj (@MEM_dec_bl _ _) (@MEM_dec_lb _ _).
Lemma MEM_beq_neq x y : (x =? y)%MEM = false <-> x <> y.
Proof. rewrite <- MEM_beq_eq; destruct (x =? y)%MEM; intuition congruence. Qed.
Global Instance MEM_beq_compat : Proper (eq ==> eq ==> eq) MEM_beq | 10.
Proof. repeat intro; subst; reflexivity. Qed.

Delimit Scope FLAG_scope with FLAG.
Bind Scope FLAG_scope with FLAG.

Infix "=?" := FLAG_beq : FLAG_scope.

Global Instance FLAG_beq_spec : reflect_rel (@eq FLAG) FLAG_beq | 10
  := reflect_of_beq internal_FLAG_dec_bl internal_FLAG_dec_lb.
Definition FLAG_beq_eq x y : (x =? y)%FLAG = true <-> x = y := conj (@internal_FLAG_dec_bl _ _) (@internal_FLAG_dec_lb _ _).
Lemma FLAG_beq_neq x y : (x =? y)%FLAG = false <-> x <> y.
Proof. rewrite <- FLAG_beq_eq; destruct (x =? y)%FLAG; intuition congruence. Qed.
Global Instance FLAG_beq_compat : Proper (eq ==> eq ==> eq) FLAG_beq | 10.
Proof. repeat intro; subst; reflexivity. Qed.

Delimit Scope OpCode_scope with OpCode.
Bind Scope OpCode_scope with OpCode.

Infix "=?" := OpCode_beq : OpCode_scope.

Global Instance OpCode_beq_spec : reflect_rel (@eq OpCode) OpCode_beq | 10
  := reflect_of_beq internal_OpCode_dec_bl internal_OpCode_dec_lb.
Definition OpCode_beq_eq x y : (x =? y)%OpCode = true <-> x = y := conj (@internal_OpCode_dec_bl _ _) (@internal_OpCode_dec_lb _ _).
Lemma OpCode_beq_neq x y : (x =? y)%OpCode = false <-> x <> y.
Proof. rewrite <- OpCode_beq_eq; destruct (x =? y)%OpCode; intuition congruence. Qed.
Global Instance OpCode_beq_compat : Proper (eq ==> eq ==> eq) OpCode_beq | 10.
Proof. repeat intro; subst; reflexivity. Qed.

Delimit Scope ARG_scope with ARG.
Bind Scope ARG_scope with ARG.

Definition ARG_beq (x y : ARG) : bool
  := match x, y with
     | reg x, reg y => REG_beq x y
     | mem x, mem y => MEM_beq x y
     | const x, const y => CONST_beq x y
     | reg _, _
     | mem _, _
     | const _, _
       => false
     end.
Global Arguments ARG_beq !_ !_ / .

Infix "=?" := ARG_beq : ARG_scope.

Lemma ARG_dec_bl (x y : ARG) : ARG_beq x y = true -> x = y.
Proof. t_dec. Qed.
Lemma ARG_dec_lb (x y : ARG) : x = y -> ARG_beq x y = true.
Proof. t_dec. Qed.
Definition ARG_eq_dec (x y : ARG) : {x = y} + {x <> y}
  := (if (x =? y)%ARG as b return (x =? y)%ARG = b -> _
      then fun pf => left (@ARG_dec_bl _ _ pf)
      else fun pf => right (fun pf' => diff_false_true (eq_trans (eq_sym pf) (@ARG_dec_lb _ _ pf'))))
       eq_refl.

Global Instance ARG_beq_spec : reflect_rel (@eq ARG) ARG_beq | 10
  := reflect_of_beq ARG_dec_bl ARG_dec_lb.
Definition ARG_beq_eq x y : (x =? y)%ARG = true <-> x = y := conj (@ARG_dec_bl _ _) (@ARG_dec_lb _ _).
Lemma ARG_beq_neq x y : (x =? y)%ARG = false <-> x <> y.
Proof. rewrite <- ARG_beq_eq; destruct (x =? y)%ARG; intuition congruence. Qed.
Global Instance ARG_beq_compat : Proper (eq ==> eq ==> eq) ARG_beq | 10.
Proof. repeat intro; subst; reflexivity. Qed.

Delimit Scope NormalInstruction_scope with NormalInstruction.
Bind Scope NormalInstruction_scope with NormalInstruction.

Definition NormalInstruction_beq (x y : NormalInstruction) : bool
  := ((x.(op) =? y.(op))%OpCode
      && list_beq _ ARG_beq x.(args) y.(args))%bool.
Global Arguments NormalInstruction_beq !_ !_ / .

Infix "=?" := NormalInstruction_beq : NormalInstruction_scope.

Lemma NormalInstruction_dec_bl (x y : NormalInstruction) : NormalInstruction_beq x y = true -> x = y.
Proof. t_dec. Qed.
Lemma NormalInstruction_dec_lb (x y : NormalInstruction) : x = y -> NormalInstruction_beq x y = true.
Proof. t_dec. Qed.
Definition NormalInstruction_eq_dec (x y : NormalInstruction) : {x = y} + {x <> y}
  := (if (x =? y)%NormalInstruction as b return (x =? y)%NormalInstruction = b -> _
      then fun pf => left (@NormalInstruction_dec_bl _ _ pf)
      else fun pf => right (fun pf' => diff_false_true (eq_trans (eq_sym pf) (@NormalInstruction_dec_lb _ _ pf'))))
       eq_refl.

Global Instance NormalInstruction_beq_spec : reflect_rel (@eq NormalInstruction) NormalInstruction_beq | 10
  := reflect_of_beq NormalInstruction_dec_bl NormalInstruction_dec_lb.
Definition NormalInstruction_beq_eq x y : (x =? y)%NormalInstruction = true <-> x = y := conj (@NormalInstruction_dec_bl _ _) (@NormalInstruction_dec_lb _ _).
Lemma NormalInstruction_beq_neq x y : (x =? y)%NormalInstruction = false <-> x <> y.
Proof. rewrite <- NormalInstruction_beq_eq; destruct (x =? y)%NormalInstruction; intuition congruence. Qed.
Global Instance NormalInstruction_beq_compat : Proper (eq ==> eq ==> eq) NormalInstruction_beq | 10.
Proof. repeat intro; subst; reflexivity. Qed.

Delimit Scope RawLine_scope with RawLine.
Bind Scope RawLine_scope with RawLine.

Definition RawLine_beq (x y : RawLine) : bool
  := match x, y with
     | SECTION x, SECTION y => String.eqb x y
     | GLOBAL x, GLOBAL y => String.eqb x y
     | LABEL x, LABEL y => String.eqb x y
     | EMPTY, EMPTY => true
     | INSTR x, INSTR y => NormalInstruction_beq x y
     | SECTION _, _
     | GLOBAL _, _
     | LABEL _, _
     | EMPTY, _
     | INSTR _, _
       => false
     end.
Global Arguments RawLine_beq !_ !_ / .

Infix "=?" := RawLine_beq : RawLine_scope.

Lemma RawLine_dec_bl (x y : RawLine) : RawLine_beq x y = true -> x = y.
Proof. t_dec. Qed.
Lemma RawLine_dec_lb (x y : RawLine) : x = y -> RawLine_beq x y = true.
Proof. t_dec. Qed.
Definition RawLine_eq_dec (x y : RawLine) : {x = y} + {x <> y}
  := (if (x =? y)%RawLine as b return (x =? y)%RawLine = b -> _
      then fun pf => left (@RawLine_dec_bl _ _ pf)
      else fun pf => right (fun pf' => diff_false_true (eq_trans (eq_sym pf) (@RawLine_dec_lb _ _ pf'))))
       eq_refl.

Global Instance RawLine_beq_spec : reflect_rel (@eq RawLine) RawLine_beq | 10
  := reflect_of_beq RawLine_dec_bl RawLine_dec_lb.
Definition RawLine_beq_eq x y : (x =? y)%RawLine = true <-> x = y := conj (@RawLine_dec_bl _ _) (@RawLine_dec_lb _ _).
Lemma RawLine_beq_neq x y : (x =? y)%RawLine = false <-> x <> y.
Proof. rewrite <- RawLine_beq_eq; destruct (x =? y)%RawLine; intuition congruence. Qed.
Global Instance RawLine_beq_compat : Proper (eq ==> eq ==> eq) RawLine_beq | 10.
Proof. repeat intro; subst; reflexivity. Qed.

Delimit Scope Line_scope with Line.
Bind Scope Line_scope with Line.

Definition Line_beq (x y : Line) : bool
  := ((x.(indent) =? y.(indent))%string
      && (x.(rawline) =? y.(rawline))%RawLine
      && (x.(pre_comment_whitespace) =? y.(pre_comment_whitespace))%string
      && option_beq String.eqb x.(comment) y.(comment))%bool.
Global Arguments Line_beq !_ !_ / .

Infix "=?" := Line_beq : Line_scope.

Lemma Line_dec_bl (x y : Line) : Line_beq x y = true -> x = y.
Proof. t_dec. Qed.
Lemma Line_dec_lb (x y : Line) : x = y -> Line_beq x y = true.
Proof. t_dec. Qed.
Definition Line_eq_dec (x y : Line) : {x = y} + {x <> y}
  := (if (x =? y)%Line as b return (x =? y)%Line = b -> _
      then fun pf => left (@Line_dec_bl _ _ pf)
      else fun pf => right (fun pf' => diff_false_true (eq_trans (eq_sym pf) (@Line_dec_lb _ _ pf'))))
       eq_refl.

Global Instance Line_beq_spec : reflect_rel (@eq Line) Line_beq | 10
  := reflect_of_beq Line_dec_bl Line_dec_lb.
Definition Line_beq_eq x y : (x =? y)%Line = true <-> x = y := conj (@Line_dec_bl _ _) (@Line_dec_lb _ _).
Lemma Line_beq_neq x y : (x =? y)%Line = false <-> x <> y.
Proof. rewrite <- Line_beq_eq; destruct (x =? y)%Line; intuition congruence. Qed.
Global Instance Line_beq_compat : Proper (eq ==> eq ==> eq) Line_beq | 10.
Proof. repeat intro; subst; reflexivity. Qed.

Delimit Scope Lines_scope with Lines.
Bind Scope Lines_scope with Lines.

Definition Lines_beq (x y : Lines) : bool
  := list_beq _ Line_beq x y.
Global Arguments Lines_beq !_ !_ / .

Infix "=?" := Lines_beq : Lines_scope.

Lemma Lines_dec_bl (x y : Lines) : Lines_beq x y = true -> x = y.
Proof. t_dec. Qed.
Lemma Lines_dec_lb (x y : Lines) : x = y -> Lines_beq x y = true.
Proof. t_dec. Qed.
Definition Lines_eq_dec (x y : Lines) : {x = y} + {x <> y}
  := (if (x =? y)%Lines as b return (x =? y)%Lines = b -> _
      then fun pf => left (@Lines_dec_bl _ _ pf)
      else fun pf => right (fun pf' => diff_false_true (eq_trans (eq_sym pf) (@Lines_dec_lb _ _ pf'))))
       eq_refl.

Global Instance Lines_beq_spec : reflect_rel (@eq Lines) Lines_beq | 10
  := reflect_of_beq Lines_dec_bl Lines_dec_lb.
Definition Lines_beq_eq x y : (x =? y)%Lines = true <-> x = y := conj (@Lines_dec_bl _ _) (@Lines_dec_lb _ _).
Lemma Lines_beq_neq x y : (x =? y)%Lines = false <-> x <> y.
Proof. rewrite <- Lines_beq_eq; destruct (x =? y)%Lines; intuition congruence. Qed.
Global Instance Lines_beq_compat : Proper (eq ==> eq ==> eq) Lines_beq | 10.
Proof. repeat intro; subst; reflexivity. Qed.

author: dip-proto

save_path: github-repos/coq/dip-proto-fiat-crypto


text:
Require Import String.
Require Import CoherenceBasicBD.
Require Import Coq.Structures.Equalities.
Require Import Coq.MSets.MSetInterface.
Require Import Arith.
Require Import Setoid.
Require Import Coq.Program.Equality.
Require Import Coq.Program.Tactics.

Module Semantics
       (Import VarTyp : BooleanDecidableType')
       (Import set : MSetInterface.S).

Module CBD := CoherenceBasicBiDi(VarTyp)(set).
Import CBD.

Inductive typing : ST.context PTyp -> PExp -> PTyp -> Prop :=
  | TyVar' : forall Gamma x ty,
               ST.ok Gamma ->
               List.In (x, ty) Gamma ->
               WFTyp ty ->
               typing Gamma (PFVar x) ty
  | TyLit' : forall Gamma i,
               ST.ok Gamma ->
               typing Gamma (PLit i) PInt
  | TyLam' : forall L Gamma t A B,
               (forall x, ~ ST.M.In x L ->
                     typing (ST.extend x A Gamma) (open_source t (PFVar x)) B) ->
               WFTyp A ->
               typing Gamma (PLam t) (Fun A B)
  | TyApp' : forall Gamma A B t1 t2,
               typing Gamma t1 (Fun A B) ->
               typing Gamma t2 A ->
               typing Gamma (PApp t1 t2) B
  | TyMerge' : forall Gamma A B t1 t2,
                 typing Gamma t1 A ->
                 typing Gamma t2 B ->
                 OrthoS A B ->
                 typing Gamma (PMerge t1 t2) (And A B)
  | TySub' : forall Gamma t A B,
               typing Gamma t A ->
               Sub A B ->
               WFTyp B ->
               typing Gamma t B.

Inductive AExp : PExp -> Prop :=
  | ALit : forall n, AExp (PLit n)
  | ALam : forall t, AExp (PLam t).

Inductive Value : PExp -> Prop :=
  | VAnn : forall a A, AExp a -> Value (PAnn RT a A)
  | VMerge : forall v1 v2, Value v1 -> Value v2 -> Value (PMerge v1 v2).

Inductive In : PExp -> PTyp -> Prop :=
  | InInt : forall n, In (PAnn RT (PLit n) PInt) PInt
  | InFun : forall e A B, In (PAnn RT (PLam e) (Fun A B)) (Fun A B)
  | InAnd : forall v1 v2 A B, In v1 A ->
                         In v2 B ->
                         OrthoS A B ->
                         In (PMerge v1 v2) (And A B).

Inductive bidityping : ST.context PTyp -> PExp -> Dir -> PTyp -> Prop :=
  | ATyVar' : forall (Gamma : ST.context PTyp) (x : ST.var) (ty : PTyp),
                ST.ok Gamma ->
                List.In (x, ty) Gamma ->
                WFTyp ty ->
                bidityping Gamma (PFVar x) Inf ty
  | ATyLit' : forall (Gamma : ST.context PTyp) (x : nat),
                ST.ok Gamma ->
                bidityping Gamma (PLit x) Inf PInt
  | ATyApp' : forall (Gamma : ST.context PTyp) (A B : PTyp) (t1 t2 : PExp),
                bidityping Gamma t1 Inf (Fun A B) ->
                bidityping Gamma t2 Chk A ->
                bidityping Gamma (PApp t1 t2) Inf B
  | ATyMerge' : forall (Gamma : ST.context PTyp) (A B : PTyp) (t1 t2 : PExp),
                  bidityping Gamma t1 Inf A ->
                  bidityping Gamma t2 Inf B ->
                  OrthoS A B ->
                  bidityping Gamma (PMerge t1 t2) Inf (And A B)
  | ATyAnnCT' : forall (Gamma : ST.context PTyp) (t1 : PExp) (A : PTyp),
                  bidityping Gamma t1 Chk A ->
                  bidityping Gamma (PAnn CT t1 A) Inf A
  | ATyAnnRT' : forall (Gamma : ST.context PTyp) (t1 : PExp) (A : PTyp),
                  bidityping Gamma t1 Chk A ->
                  bidityping Gamma (PAnn RT t1 A) Inf A
  | ATyLam' : forall (L : ST.M.t) (Gamma : ST.context PTyp)
                (t : PExp) (A B : PTyp),
                (forall x : ST.M.elt,
                   ~ ST.M.In x L ->
                   bidityping (ST.extend x A Gamma) (open_source t (PFVar x)) Chk B) ->
                WFTyp A ->
                bidityping Gamma (PLam t) Chk (Fun A B)
  | ATySub' : forall (Gamma : ST.context PTyp) (t : PExp)
                (A B : PTyp) (C : ST.Exp),
                bidityping Gamma t Inf A ->
                sub A B C ->
                WFTyp B ->
                bidityping Gamma t Chk B.

Inductive red : PExp -> PExp -> Prop :=
  | Red_Int : forall n, red (PLit n) (PAnn RT (PLit n) PInt)
  | Red_Abs : forall e A B,
                red (PAnn CT (PLam e) (Fun A B))
                    (PAnn RT (PLam e) (Fun A B))
  | Red_App1 : forall e1 e2 e3,
                 red e1 e3 ->
                 red (PApp e1 e2) (PApp e3 e2)
  | Red_App2 : forall e1 e2 v,
                 Value v ->
                 red e1 e2 ->
                 red (PApp v e1) (PApp v e2)
  | Red_App3 : forall A B v1 v2,
                 Value v1 ->
                 Value v2 ->
                 In v1 (Fun A B) ->
                 not (In v2 A) ->
                 red (PApp v1 v2) (PApp v1 (PAnn CT v2 A))
  | Red_App4 : forall A B e v,
                 Value v ->
                 In v A ->
                 red (PApp (PAnn RT (PLam e) (Fun A B)) v)
                     (PAnn CT (open_source e v) B)
  | Red_Merge1 : forall e1 e2 e3,
                   red e1 e3 ->
                   red (PMerge e1 e2) (PMerge e3 e2)
  | Red_Merge2 : forall e1 e2 v,
                   Value v ->
                   red e1 e2 ->
                   red (PMerge v e1) (PMerge v e2)
  | Red_Ann : forall e1 e2 A,
                red e1 e2 ->
                red (PAnn CT e1 A) (PAnn CT e2 A)
  | ARed_Int : forall n,
                    red (PAnn CT (PAnn RT (PLit n) PInt) PInt)
                        (PAnn RT (PLit n) PInt)
  | ARed_Fun :
      forall e A B C D,
        red (PAnn CT (PAnn RT (PLam e) (Fun A B)) (Fun C D))
            (PAnn RT (PLam (PAnn CT (PApp (PAnn RT (PLam e) (Fun A B))
                                          (PAnn CT (PBVar 0) A)) D))
                  (Fun C D))
  | ARed_Merge1 : forall v1 v2 A B,
                    Sub A B ->
                    Atomic B ->
                    Value v1 ->
                    Value v2 ->
                    In v1 A ->
                    red (PAnn CT (PMerge v1 v2) B)
                        (PAnn CT v1 B)
  | ARed_Merge2 : forall v1 v2 A B,
                    Sub A B ->
                    Atomic B ->
                    Value v1 ->
                    Value v2 ->
                    In v2 A ->
                    red (PAnn CT (PMerge v1 v2) B)
                        (PAnn CT v2 B)
  | ARed_Merge3 : forall v A B,
                    Value v ->
                    red (PAnn CT v (And A B))
                        (PMerge (PAnn CT v A) (PAnn CT v B)).

Hint Constructors typing bidityping AExp Value In WFTyp red.

(** Soundness and Completeness wrt to the elaborating biditypecheker **)

Theorem has_type_source_alg_rename :
  forall L Gamma A B t1 c m y,
    has_type_source_alg (ST.extend y A Gamma) (open_source t1 (PFVar y)) B m
                        (ST.open c (ST.STFVar _ y)) ->
    (forall x, ~ ST.M.In x L ->
          has_type_source_alg (ST.extend x A Gamma) (open_source t1 (PFVar x)) B m
                              (ST.open c (ST.STFVar _ x))).
Proof.
  intros.
  (* subst_typ_source_intro *)
Admitted.

Theorem soundness : forall Gamma e A m, bidityping Gamma e A m -> has_ty Gamma e A m.
Proof.
  intros Gamma e A m H; unfold has_ty.
  induction H; destruct_conjs; eauto.
  - ST.pick_fresh x.
    destruct (H0 _ Fr) as [c H2].
    exists (ST.STLam' _ c).
    apply_fresh ATyLam as z; auto.
    apply has_type_source_alg_rename with (L := L) (y := x).
    admit. (* missing the good old renaming lemma... *)
    ST.not_in_L z.
Admitted.

Theorem completeness :
  forall Gamma A m d e, has_type_source_alg Gamma e A m d -> bidityping Gamma e A m.
Proof. intros Gamma A m d e H; induction H; eauto; destruct m; auto. Qed.

Hint Resolve soundness completeness.

(** Some necessary properties about bidityping, which are lifted from
    the elaborated version **)

Theorem bityping_ok : forall Gamma t A m, bidityping Gamma t m A -> ST.ok Gamma.
Proof.
  intros; apply soundness in H as [c H]; eapply typing_alg_ok_env; eauto.
Qed.

Theorem bityping_wf : forall Gamma t A m, bidityping Gamma t m A -> WFTyp A.
Proof.
  intros; apply soundness in H as [c H]; eapply typing_wf_source_alg; eauto.
Qed.

Theorem bityping_term : forall Gamma e A m, bidityping Gamma e m A -> PTerm e.
Proof.
  intros; apply soundness in H as [c H]; eapply type_correct_alg_terms; eauto.
Qed.

Theorem bityping_weaken:
  forall G E F t T dir, bidityping (E ++ G) t dir T ->
                   ST.ok (E ++ F ++ G) ->
                   bidityping (E ++ F ++ G) t dir T.
Proof.
  intros; apply soundness in H as [c H].
  assert (Ha := typing_weaken_alg _ _ _ _ _ _ _ H H0); eauto.
Qed.

(* We didn't prove this before?! *)
Theorem sub_trans : forall A B, Sub A B -> forall C, Sub B C -> Sub A C. Admitted.

Hint Resolve bityping_ok bityping_wf bityping_term bityping_weaken
     reflex sub_trans.
Hint Unfold Sub.

(*
Theorem bityping_ann_sub :
  forall Gamma t A B m1 m2, bidityping Gamma (PAnn m1 t A) m2 B -> Sub A B.
Proof. intros Gamma t A B m1 m2 Htyping; dependent induction Htyping; eauto. Qed.

Theorem bityping_ann :
  forall Gamma t A B m1 m2, bidityping Gamma (PAnn m1 t A) B m2 -> bidityping Gamma t Chk A.
Proof. intros Gamma t A B m1 m2 Htyping; dependent induction Htyping; eauto. Qed.
*)

(** Properties mixing "Sub", "In" and the type-system. **)

Theorem In_Ann_inv : forall a A B, AExp a -> In (PAnn RT a A) B -> A = B.
Proof. intros v A B H1 H2; dependent induction H2; auto. Qed.

(*Hint Resolve bityping_ann_sub bityping_ann.*)
Hint Resolve In_Ann_inv.
Hint Unfold erase.

Theorem In_bityping_sub :
  forall A v, In v A -> forall B Gamma, bidityping Gamma v Inf B -> Sub A B.
Proof.
  intros A v HIn.
  induction HIn; eauto 3.
  - intros; inversion H; subst; eauto.
  - intros; inversion H; subst; eauto.
  - intros; dependent induction H0.
    clear IHbidityping1 IHbidityping2.
    apply IHHIn1 in H0_.
    apply IHHIn2 in H0_0.
    auto.
Qed.

Hint Resolve In_bityping_sub.

Theorem In_sub_bityping :
  forall Gamma B A e, Sub A B ->
             In e A ->
             bidityping Gamma e Inf B ->
             bidityping Gamma e Inf A.
Proof.
  intros Gamma B A e HSub HIn Hbidi.
  generalize dependent A.
  induction Hbidi; intros; try now inversion HIn.
  - apply invAndS1 in HSub. destruct HSub.
    inversion HIn; subst.
    assert (Ha1 : Sub A1 A) by eauto.
    assert (Ha2 : Sub B0 B) by eauto.
    assert (Ha3 : bidityping Gamma t1 Inf A1) by auto.
    assert (Ha4 : bidityping Gamma t2 Inf B0) by auto.
    auto. (* since Value implies disjointness *)
  - inversion HIn; subst; eauto.
  - assert (Ha1 : Sub A0 A) by eauto.
    assert (Ha2 : bidityping Gamma t0 Inf A0) by auto.
    assert (Ha3 : Sub A0 A0) by apply reflex.
    destruct Ha3; eauto.
Qed.

Hint Resolve In_sub_bityping.

Theorem In_bityping :
  forall Gamma A B e, In e A -> bidityping Gamma e Inf B -> bidityping Gamma e Inf A.
Proof.
  intros Gamma A B e HIn Htyping.
  assert (Sub A B) by eauto.
  eapply In_sub_bityping; eauto.
Qed.

Hint Resolve In_bityping.

Theorem bityping_inf_chk :
  forall Gamma e A,
    bidityping Gamma e Inf A -> bidityping Gamma e Chk A.
Proof.
  intros Gamma e A Htyping.
  assert (Ha : Sub A A) by eauto; destruct Ha.
  eapply ATySub' with (A := A); eauto.
Qed.

Hint Resolve bityping_inf_chk.

(** Defining body. (getting ready for subject reduction) **)

Definition body_bityping Gamma t A B :=
  exists L, forall x, not (ST.M.In x L) ->
            bidityping (ST.extend x A Gamma) (open_source t (PFVar x)) Chk B.

Hint Unfold body_bityping.

Lemma abs_to_body_bityping : forall A B e Gamma,
  bidityping Gamma (PLam e) Chk (Fun A B) -> body_bityping Gamma e A B.
Proof. intros; inversion H; subst; eauto; inversion H0. Qed.

Lemma open_body_bityping :
  forall e A B u Gamma, body_bityping Gamma e A B -> WFTyp A ->
               bidityping Gamma (open_source e u) Chk B.
Proof.
  intros e A B u Gamma H1 H2; destruct H1. pick_fresh y.
  assert (Ha : not (ST.M.In y x)) by ST.not_in_L y; apply H in Ha.
  admit. (* needs subst, weakening, etc... *)
Admitted.

Hint Resolve open_body_bityping.

(** Theorem 1. Subject reduction **)

Theorem subject_reduction :
  forall Gamma e1 A m, bidityping Gamma e1 m A ->
              forall e2, red e1 e2 ->
                    bidityping Gamma e2 m A.
Proof.
  intros Gamma e1 A m Htyping e2 Hred;
  generalize dependent A; generalize dependent Gamma; generalize dependent m.
  induction Hred; intros; try now (dependent induction Htyping; subst; eauto).
  - (* R_App3 *)
    dependent induction Htyping; subst; eauto.
    apply ATyApp' with (A := A); auto; clear IHHtyping1 IHHtyping2.
    + inversion Htyping1; subst; try now inversion H.
      inversion H1; subst.
      eauto.
    + apply bityping_inf_chk.
      apply ATyAnnCT'.
      inversion Htyping2; subst. inversion H0.
      assert (Ha : Sub (Fun A B) (Fun A0 B0)) by eauto.
      destruct Ha; inversion H6; subst.
      assert (Ha1 : Sub A0 A) by eauto.
      assert (Ha2 : Sub A1 A0) by eauto.
      assert (Ha3 : Sub A1 A) by eauto; destruct Ha3.
      eapply ATySub' with (A := A1); eauto 3.
      assert (Ha4 : bidityping Gamma v1 Inf (Fun A B)) by eauto.
      apply bityping_wf in Ha4; now inversion Ha4.
  - (* R_App4 *)
    dependent induction Htyping; subst; eauto.
    clear IHHtyping1 IHHtyping2.
    inversion Htyping1; subst.
    apply ATyAnnCT'; clear Htyping1.
    apply open_body_bityping with (A := A0); eauto.
    inversion H5; subst; eauto.
    inversion H1.
  - (* A_Abs *)
    dependent induction Htyping; subst; eauto; clear IHHtyping.
    inversion Htyping; subst.
    inversion H; subst.
    inversion H1; subst.
    apply ATyAnnRT'.
    apply_fresh ATyLam' as x; auto.
    unfold open_source; simpl.
    assert (Ha : Sub D D) by apply reflex; destruct Ha.
    assert (Ha : WFTyp A) by
        (now assert (Ha := bityping_wf _ _ _ _ H); inversion Ha).
    eapply ATySub' with (A := D); eauto 2.
    apply ATyAnnCT'.
    inversion H0; subst; clear H0.
    eapply ATySub' with (A := B); eauto 2.
    eapply ATyApp' with (A := A).
    + apply ATyAnnRT'.
      change (PLam (open_rec_source 1 (PFVar x) e)) with
             ((open_rec_source 0 (PFVar x) (PLam e))).
      rewrite <- open_rec_source_term; eauto 3.
      rewrite <- app_nil_l with (l := (ST.extend x C Gamma)).
      apply bityping_weaken; simpl; auto.
      apply ST.Ok_push; eauto.
      ST.not_in_L x.
    + assert (Ha1 : Sub A A) by apply reflex; destruct Ha1.
      eapply ATySub' with (A := A); eauto 2.
      apply ATyAnnCT'.
      eapply ATySub' with (A := C); eauto 2.
      apply ATyVar'; auto.
      apply ST.Ok_push; eauto.
      ST.not_in_L x.
      now left.
  - (* A_Merge1 *)
    dependent induction Htyping; subst; eauto; clear IHHtyping.
    inversion Htyping; subst.
    inversion H4; subst.
    apply ATyAnnCT'.
    assert (Ha : bidityping Gamma v1 Inf A) by eauto.
    destruct H; eauto.
  - (* A_Merge2 *)
    dependent induction Htyping; subst; eauto; clear IHHtyping.
    inversion Htyping; subst.
    inversion H4; subst.
    apply ATyAnnCT'.
    assert (Ha : bidityping Gamma v2 Inf B0) by eauto.
    destruct H; eauto.
  - (* A_Merge3 *)
    dependent induction Htyping; subst; eauto; clear IHHtyping.
    inversion Htyping; subst.
    inversion H2; subst.
    assert (HSub : Sub A0 (And A B)) by eauto.
    apply invAndS1 in HSub; destruct HSub; destruct H3; destruct H4.
    apply ATyMerge'; eauto.
Qed.

(** Theorem 2. All typeable terms can reduce **)

Theorem typeable_terms_reduce :
  forall e1 A, bidityping nil e1 Inf A -> exists e2, red e1 e2.
Proof.
  intros e1 A H.
  dependent induction H; eauto.
  - inversion H0.
  - assert (Ha1 : exists e2 : PExp, red t1 e2) by eauto.
    destruct Ha1; eauto.
  - assert (Ha1 : exists e2 : PExp, red t1 e2) by eauto.
    assert (Ha2 : exists e2 : PExp, red t2 e2) by eauto.
    destruct Ha1, Ha2; eauto.
  - assert (Ha1 : exists e2  : PExp, red t1 e2) by eauto.
    destruct Ha1; eauto.
  - assert (Ha1 : exists e2  : PExp, red t1 e2) by eauto.
    destruct Ha1.
    admit. (* missing assumption that terms do not contain RT anns? *)
  - admit. (* abs case *)
Admitted.

End Semantics.

author: zhiyuanshi

repo: intersection


text:
Require Import Iron.Language.SystemF2.Step.
Require Import Iron.Language.SystemF2.SubstExpExp.
Require Import Iron.Language.SystemF2.SubstTypeExp.
Require Import Iron.Language.SystemF2.SubstTypeType.
Require Import Iron.Language.SystemF2.TyJudge.

(* A closed, well typed expression is either a value
   or can take a step. *)
Theorem progress
 :  forall x
 ,  (exists t, TYPE nil nil x t)
 -> value x \/ (exists x', STEP x x').
Proof.
 intros.
 induction x; destruct H as [tx].

 Case "XVar".
  inverts H. false.

 Case "XLAM".
  left. apply type_wfX in H. auto.

 Case "XAPP".
  inverts H.
  destruct IHx. eauto.
  SCase "x value".
   right. inverts H. inverts H4.
    inverts H1. false.
    inverts H0.
    exists (substTX 0 t x1). eapply ESLAMAPP.
    inverts H0.
  SCase "x steps".
   right.
    destruct H as [x'].
    exists (XAPP x' t).
    apply ESAPP1. auto.

 Case "XLam".
  left. apply type_wfX in H. auto.

 Case "XApp".
  right.
  inverts H.
  destruct IHx1; eauto.
  SCase "x1 value".
   destruct IHx2; eauto.
   inverts H.

   SSCase "x2 value".
    inverts H1.
     inverts H2. false.
     inverts H4.
     exists (substXX 0 x2 x0).
      inverts H0. apply ESLamApp. auto.

   SSCase "x2 steps".
    destruct H0 as [x2'].
    exists (XApp x1 x2').
     inverts H. apply ESApp2; auto.

  SCase "x1 steps".
   destruct H as [x1'].
   exists (XApp x1' x2).
   apply ESApp1; auto.
Qed.

author: DonaldKellett

repo: iron-lambda