text:
Require Import Arith.
Require Import Ensembles.
Require Import Coq.Lists.List.

Require Import Languages.
Require Import folProof.
Require Import folProp.
Require Import folLogic3.

Definition Formula := Formula LNT.
Definition Formulas := Formulas LNT.
Definition System := System LNT.
Definition Sentence := Sentence LNT.
Definition Term := Term LNT.
Definition Terms := Terms LNT.
Definition SysPrf := SysPrf LNT.
#[local] Arguments apply _ _ _ : clear implicits.

Definition Plus (x y : Term) : Term :=
  apply LNT Plus_ (Tcons x (Tcons y (Tnil))).

Definition Times (x y : Term) : Term :=
  apply LNT Times_ (Tcons x (Tcons y (Tnil))).

Definition Succ (x : Term) : Term :=
  apply LNT Succ_ (Tcons x (Tnil)).

Definition Zero : Term := apply LNT Zero_ (Tnil).

(** Notations for LNT formulas: experimental and unstable *)

Declare Scope nt_scope.
Delimit Scope nt_scope with nt.

Infix "=" := (equal _): nt_scope.
Infix "\/" := (orH): nt_scope.
Infix "/\" := (andH):nt_scope.
Infix "->" := (impH): nt_scope.
Notation "~ A" := (@notH _ A): nt_scope.
Notation "A <-> B" := (@iffH _ A B): nt_scope.

Notation k_ t := (apply  (t:Functions _)  (Tnil)).

Notation app1 f arg :=
  (apply  (f: Functions _)  (Tcons arg (Tnil))).
About Tnil.
Notation app2 f arg1 arg2 :=
  (apply   (f: Functions _)
     (Tcons  arg1 (Tcons  arg2 (Tnil)))).

Notation "t = u" := (@equal _ t u): nt_scope.
Notation "t <> u" := (~ t = u)%nt : nt_scope.

Reserved Notation "x '\/'' y" (at level 85, right associativity).
Reserved Notation "x '/\'' y" (at level 80, right associativity).
Reserved Notation "x '<->'' y" (at level 95, no associativity).
Reserved Notation "x '<->''' y" (at level 95, no associativity).

Notation "x \/' y" := (~ x -> y)%nt : nt_scope.
Notation "x /\' y" := (~ (~ x \/'  ~ y))%nt : nt_scope.
Notation "x <->'' y" := ((x -> y) /\ (y -> x))%nt:  nt_scope.
Notation "x <->' y" := (~ (~ (x -> y) \/' ~(y -> x)))%nt : nt_scope.

(* Notation exH := (existH). *)
Notation "'v_' i" := (var i) (at level 3) : nt_scope.

Notation exH' v A := (~ (forallH v (~ A)))%nt.

Notation "'exH' x .. y , p" := (existH  x .. (existH y p) ..)
  (x at level 0, y at level 0, at level 200, right associativity) : nt_scope.

Notation "'allH' x .. y , p" := (forallH  x .. (forallH y p) ..)
  (x at level 0, y at level 0, at level 200, right associativity) : nt_scope.

Module NTnotations.
Infix "+" := Plus :nt_scope.
Infix "*" := Times :nt_scope.
End NTnotations.

Export NTnotations.

Section Examples.
Variable f : Formula.
Check (allH 0 1 ,  (f -> v_ 0 = v_ 0 -> v_ 1 = v_ 1))%nt.

Check (exH 0 1 ,  (v_ 0 = v_ 0 -> v_ 1 = v_ 1))%nt.
End Examples.

Lemma LNT_dec : language_decidable LNT.
Proof. split; decide equality. Qed.

Section Free_Variables.

Lemma freeVarPlus (x y: Term) :
 freeVarTerm LNT (Plus x y) = freeVarTerm LNT x ++ freeVarTerm LNT y.
Proof.
  now rewrite (app_nil_end (freeVarTerm LNT y)).
Qed.

Lemma freeVarTimes (x y : Term) :
 freeVarTerm LNT (Times x y) = freeVarTerm LNT x ++ freeVarTerm LNT y.
Proof.
  now rewrite (app_nil_end (freeVarTerm LNT y)).
Qed.

Lemma freeVarSucc (x : Term):
  freeVarTerm LNT (Succ x) = freeVarTerm LNT x.
Proof.
  now rewrite (app_nil_end (freeVarTerm LNT x)).
Qed.

Lemma freeVarZero : freeVarTerm LNT Zero = nil.
Proof. reflexivity. Qed.

End Free_Variables.

Section Logic.

Lemma Axm  (T : System) (f : Formula) :  mem _ T f -> SysPrf T f.
Proof. apply (Axm LNT). Qed.

Lemma sysExtend (T U : System) (f : Formula):
  Included _ T U -> SysPrf T f -> SysPrf U f.
Proof. apply (sysExtend LNT). Qed.

Lemma sysWeaken (T : System) (f g : Formula):
  SysPrf T f -> SysPrf (Ensembles.Add _ T g) f.
Proof. apply (sysWeaken LNT). Qed.

Lemma impI (T : System) (f g : Formula):
  SysPrf (Ensembles.Add _ T g) f -> SysPrf T (impH g f).
Proof. apply (impI LNT). Qed.

Lemma impE (T : System) (f g : Formula):
 SysPrf T (impH g f) -> SysPrf T g -> SysPrf T f.
Proof. apply (impE LNT). Qed.

Lemma contradiction (T : System) (f g : Formula):
 SysPrf T f -> SysPrf T (notH f) -> SysPrf T g.
Proof. apply (contradiction LNT). Qed.

Lemma nnE (T : System) (f : Formula):
  SysPrf T (notH (notH f)) -> SysPrf T f.
Proof. apply (nnE LNT). Qed.

Lemma noMiddle (T : System) (f : Formula): SysPrf T (orH (notH f) f).
Proof. apply (noMiddle LNT). Qed.

Lemma nnI (T : System) (f : Formula):
  SysPrf T f -> SysPrf T (notH (notH f)).
Proof. apply (nnI LNT). Qed.

Lemma cp1 (T : System) (f g : Formula):
 SysPrf T (impH (notH f) (notH g)) -> SysPrf T (impH g f).
Proof. apply (cp1 LNT). Qed.

Lemma cp2 (T : System) (f g : Formula):
 SysPrf T (impH g f) -> SysPrf T (impH (notH f) (notH g)).
Proof. apply (cp2 LNT). Qed.

Lemma orI1 (T : System) (f g : Formula):
  SysPrf T f -> SysPrf T (orH f g).
Proof. apply (orI1 LNT). Qed.

Lemma orI2 (T : System) (f g : Formula):
  SysPrf T g -> SysPrf T (orH f g).
Proof. apply (orI2 LNT). Qed.

Lemma orE (T : System) (f g h : Formula):
 SysPrf T (orH f g) ->
 SysPrf T (impH f h) -> SysPrf T (impH g h) -> SysPrf T h.
Proof. apply (orE LNT). Qed.

Lemma orSys (T : System) (f g h : Formula):
 SysPrf (Ensembles.Add _ T f) h ->
 SysPrf (Ensembles.Add _ T g) h ->
 SysPrf (Ensembles.Add _ T (orH f g)) h.
Proof. apply (orSys LNT). Qed.

Lemma andI (T : System) (f g : Formula) :
 SysPrf T f -> SysPrf T g -> SysPrf T (andH f g).
Proof. apply (andI LNT). Qed.

Lemma andE1 (T : System) (f g : Formula) :
  SysPrf T (andH f g) -> SysPrf T f.
Proof. apply (andE1 LNT). Qed.

Lemma andE2 (T : System) (f g : Formula) :
  SysPrf T (andH f g) -> SysPrf T g.
Proof. apply (andE2 LNT). Qed.

Lemma iffI (T : System) (f g : Formula) :
 SysPrf T (impH f g) -> SysPrf T (impH g f) -> SysPrf T (iffH f g).
Proof. apply (iffI LNT). Qed.

Lemma iffE1 (T : System) (f g : Formula):
 SysPrf T (iffH f g) -> SysPrf T (impH f g).
Proof. apply (iffE1 LNT). Qed.

Lemma iffE2 (T : System) (f g : Formula) :
 SysPrf T (iffH f g) -> SysPrf T (impH g f).
Proof. apply (iffE2 LNT). Qed.

Lemma forallI (T : System) (f : Formula) (v : nat):
 ~ In_freeVarSys LNT v T -> SysPrf T f -> SysPrf T (forallH v f).
Proof. apply (forallI LNT). Qed.

Lemma forallE (T : System) (f : Formula) (v : nat) (t : Term) :
 SysPrf T (forallH v f) -> SysPrf T (substituteFormula LNT f v t).
Proof. apply (forallE LNT). Qed.

Lemma forallSimp (T : System) (f : Formula) (v : nat):
 SysPrf T (forallH v f) -> SysPrf T f.
Proof. apply (forallSimp LNT). Qed.

Lemma existI (T : System) (f : Formula) (v : nat) (t : Term):
 SysPrf T (substituteFormula LNT f v t) -> SysPrf T (existH v f).
Proof. apply (existI LNT). Qed.

Lemma existE (T : System) (f g : Formula) (v : nat):
  ~ In_freeVarSys LNT v T ->
  ~ In v (freeVarFormula LNT g) ->
  SysPrf T (existH v f) -> SysPrf T (impH f g) -> SysPrf T g.
Proof. apply (existE LNT). Qed.

Lemma existSimp (T : System) (f : Formula) (v : nat):
 SysPrf T f -> SysPrf T (existH v f).
Proof. apply (existSimp LNT). Qed.

Lemma existSys (T : System) (f g : Formula) (v : nat):
  ~ In_freeVarSys LNT v T ->
  ~ In v (freeVarFormula LNT g) ->
  SysPrf (Ensembles.Add _ T f) g ->
  SysPrf (Ensembles.Add _ T (existH v f)) g.
Proof. apply (existSys LNT). Qed.

Lemma absurd1 (T : System) (f : Formula):
 SysPrf T (impH f (notH f)) -> SysPrf T (notH f).
Proof. apply (absurd1 LNT). Qed.

Lemma nImp (T : System) (f g : Formula):
 SysPrf T (andH f (notH g)) -> SysPrf T (notH (impH f g)).
Proof. apply (nImp LNT). Qed.

Lemma nOr (T : System) (f g : Formula):
 SysPrf T (andH (notH f) (notH g)) -> SysPrf T (notH (orH f g)).
Proof. apply (nOr LNT). Qed.

Lemma nAnd (T : System) (f g : Formula):
 SysPrf T (orH (notH f) (notH g)) -> SysPrf T (notH (andH f g)).
Proof. apply (nAnd LNT). Qed.

Lemma nForall (T : System) (f : Formula) (v : nat) :
 SysPrf T (existH v (notH f)) -> SysPrf T (notH (forallH v f)).
Proof. apply (nForall LNT). Qed.

Lemma nExist (T : System) (f : Formula) (v : nat):
 SysPrf T (forallH v (notH f)) -> SysPrf T (notH (existH v f)).
Proof. apply (nExist LNT). Qed.

Lemma impRefl (T : System) (f : Formula): SysPrf T (impH f f).
Proof. apply (impRefl LNT). Qed.

Lemma impTrans (T : System) (f g h : Formula):
 SysPrf T (impH f g) -> SysPrf T (impH g h) -> SysPrf T (impH f h).
Proof. apply (impTrans LNT). Qed.

Lemma orSym (T : System) (f g : Formula):
 SysPrf T (orH f g) -> SysPrf T (orH g f).
Proof. apply (orSym LNT). Qed.

Lemma andSym (T : System) (f g : Formula) :
 SysPrf T (andH f g) -> SysPrf T (andH g f).
Proof. apply (andSym LNT). Qed.

Lemma iffRefl (T : System) (f : Formula) : SysPrf T (iffH f f).
Proof. apply (iffRefl LNT). Qed.

Lemma iffSym (T : System) (f g : Formula):
 SysPrf T (iffH f g) -> SysPrf T (iffH g f).
Proof. apply (iffSym LNT). Qed.

Lemma iffTrans (T : System) (f g h : Formula):
 SysPrf T (iffH f g) -> SysPrf T (iffH g h) -> SysPrf T (iffH f h).
Proof. apply (iffTrans LNT). Qed.

Lemma eqRefl  (T : System) (a : Term): SysPrf T (equal a a).
Proof. apply (eqRefl LNT). Qed.

Lemma eqSym (T : System) (a b : Term):
 SysPrf T (equal a b) -> SysPrf T (equal b a).
Proof. apply (eqSym LNT). Qed.

Lemma eqTrans (T : System) (a b c : Term):
 SysPrf T (equal a b) -> SysPrf T (equal b c) -> SysPrf T (equal a c).
Proof. apply (eqTrans LNT). Qed.

Lemma eqPlus (T : System) (a b c d : Term):
  SysPrf T (equal a b) ->
  SysPrf T (equal c d) -> SysPrf T (equal (Plus a c) (Plus b d)).
Proof.
  intros H H0; unfold Plus.
  apply (equalFunction LNT).
  simpl in |- *.
  destruct (consTerms LNT 1 (Tcons a (Tcons c (Tnil))))as [(a0,b0) p].
  simpl; destruct (consTerms LNT 1 (Tcons b (Tcons d (Tnil))))
    as [(a1,b1) p0].
  simpl in |- *.
  destruct (consTerms LNT 0 b0) as [(a2,b2) p1].
  simpl in |- *.
  destruct (consTerms LNT 0 b1) as [(a3,b3) p2].
  simpl in |- *; repeat split.
  - simpl in p.
    inversion p.
    simpl in p0.
    inversion p0.
    apply H.
  - simpl in p.
    inversion p.
    rewrite <- p1 in H3.
    simpl in H3.
    inversion H3.
    simpl in p0.
    inversion p0.
    rewrite <- p2 in H7.
    inversion H7.
    apply H0.
Qed.

Lemma eqTimes  (T : System) (a b c d : Term):
 SysPrf T (equal a b) ->
 SysPrf T (equal c d) -> SysPrf T (equal (Times a c) (Times b d)).
Proof.
  intros H H0; unfold Times in |- *.
  apply (equalFunction LNT); simpl in |- *.
  destruct (consTerms LNT 1 (Tcons a (Tcons c (Tnil))))as [(a0,b0) p].
  simpl in |- *.
  destruct (consTerms LNT 1 (Tcons b (Tcons d (Tnil)))) as [(a1,b1) p0].
  simpl; destruct (consTerms LNT 0 b0) as [(a2,b2) p1].
  simpl ; destruct (consTerms LNT 0 b1) as [(a3,b3) p2].
  simpl in |- *; repeat split.
  - simpl in p.
    inversion p.
    simpl in p0.
    inversion p0.
    apply H.
  - simpl in p.
    inversion p.
    rewrite <- p1 in H3.
    simpl in H3.
    inversion H3.
    simpl in p0.
    inversion p0.
    rewrite <- p2 in H7.
    inversion H7.
    apply H0.
Qed.

Lemma eqSucc (T : System) (a b : Term):
 SysPrf T (a = b)%nt -> SysPrf T (Succ a = Succ b)%nt.
Proof.
  intros H; unfold Succ in |- *; apply (equalFunction LNT).
  simpl in |- *.
  destruct (consTerms LNT 0 (Tcons a (Tnil))) as [(a0,b0) p].
  simpl in |- *;
    destruct (consTerms LNT 0 (Tcons b (Tnil))) as [(a1,b1) p0].
  simpl in |- *; repeat split.
  - simpl in p.
    inversion p.
    simpl in p0.
    inversion p0.
    apply H.
Qed.

End Logic.

Fixpoint natToTerm (n : nat) : Term :=
  match n with
  | O => Zero
  | S m => Succ (natToTerm m)
  end.

Lemma closedNatToTerm :
 forall a v : nat, ~ In v (freeVarTerm LNT (natToTerm a)).
Proof.
  intros a v; induction a as [| a Hreca].
  - cbn; auto.
  - simpl; now rewrite freeVarSucc.
Qed.

author: coq-community

repo: hydra-battles


text:
Require Import Coq.Logic.Classical_Prop.
Require Import Coq.Classes.RelationClasses.
Require Import Coq.Relations.Relation_Definitions.
Require Import Logic.lib.Ensembles_ext.
Require Import Logic.GeneralLogic.Base.
Require Import Logic.GeneralLogic.KripkeModel.
Require Import Logic.GeneralLogic.Semantics.Kripke.
Require Import Logic.MinimunLogic.Syntax.
Require Import Logic.MinimunLogic.Semantics.Kripke.
Require Import Logic.PropositionalLogic.Syntax.
Require Import Logic.PropositionalLogic.Semantics.Kripke.
Require Import Logic.PropositionalLogic.DeepEmbedded.PropositionalLanguage.

Import PropositionalLanguage.

Record frame: Type := {
  underlying_set:> Type;
  underlying_relation: relation underlying_set
}.

Infix "<=" := (underlying_relation _): TheKripkeSemantics.

Local Open Scope TheKripkeSemantics.

Definition sem (f: frame) := @Ensemble (underlying_set f).

Section KripkeSemantics.

Context {Sigma: PropositionalVariables}.

Definition denotation (F: frame) (eval: Var -> sem F): expr Sigma -> sem F :=
  fix denotation (x: expr Sigma): sem F:=
  match x with
  | andp y z => @Semantics.andp F (denotation y) (denotation z)
  | orp y z => @Semantics.orp F (denotation y) (denotation z)
  | impp y z => @Semantics.impp F (underlying_relation F) (denotation y) (denotation z)
  | falsep => @Semantics.falsep F
  | varp p => eval p
  end.

Record Kmodel : Type := {
  underlying_frame :> frame;
  sem_var: Var -> sem underlying_frame
}.

Record model: Type := {
  underlying_model :> Kmodel;
  elm: underlying_model
}.

Instance MD: Model := Build_Model model.

Instance kMD: KripkeModel MD :=
  Build_KripkeModel _
    Kmodel
    (fun M => M)
    (fun M m => Build_model M m).

Instance R (M: Kmodel): Relation (Kworlds M) :=
  @underlying_relation M.

Definition Kmodel_Monotonic: Kmodel -> Prop := fun M =>
  forall v: Var, upwards_closed_Kdenote (sem_var M v).

Definition Kmodel_PreOrder: Kmodel -> Prop := fun M =>
  PreOrder (@Krelation _ (R M)).

Definition Kmodel_Identity: Kmodel -> Prop := fun M =>
  IdentityKripkeIntuitionisticModel (Kworlds M).

Definition Kmodel_NoBranch: Kmodel -> Prop := fun M =>
  NoBranchKripkeIntuitionisticModel (Kworlds M).

Definition Kmodel_BranchJoin: Kmodel -> Prop := fun M =>
  BranchJoinKripkeIntuitionisticModel (Kworlds M).

Instance SM: Semantics L MD :=
  Build_Semantics L MD (fun x M => (denotation M (sem_var M) x) (elm M)).

Instance kiSM (M: Kmodel) {_: Kmodel_Monotonic M} {_: Kmodel_PreOrder M}:
  KripkeIntuitionisticSemantics L MD M SM.
Proof.
  hnf in H, H0.
  constructor; intros.
  induction x.
  + apply Semantics.andp_closed; auto.
  + apply Semantics.orp_closed; auto.
  + apply (Semantics.impp_closed _ _ IHx1 IHx2).
  + apply Semantics.falsep_closed.
  + apply H.
Qed.

Instance kminSM (M: Kmodel): KripkeMinimunSemantics L MD M SM.
Proof.
  apply Build_KripkeMinimunSemantics.
  intros; apply Same_set_refl.
Defined.

Instance kpSM (M: Kmodel): KripkePropositionalSemantics L MD M SM.
Proof.
  apply Build_KripkePropositionalSemantics.
  + intros; apply Same_set_refl.
  + intros; apply Same_set_refl.
  + intros; apply Same_set_refl.
Defined.

End KripkeSemantics.

author: princeton-vl

repo: CoqGym

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


text:
Require Import Coq.Lists.List.
Require Import Coq.Program.Basics.
Require Import CertiGraph.lib.Coqlib.
Require Import CertiGraph.graph.graph_model.
Require Import CertiGraph.lib.EquivDec_ext.

Generalizable All Variables.

Record pregraph_isomorphism_explicit
       `(g: @PreGraph V E EV EE) `(g': @PreGraph V' E' EV' EE')
       (vmap: V -> V') (vmap': V' -> V) (emap: E -> E') (emap': E' -> E): Prop :=
  {
    vertex_bij: bijective vmap vmap';
    edge_bij: bijective emap emap';
    vvalid_bij: forall v, vvalid g v -> vvalid g' (vmap v);
    vvalid_bij_inv: forall v', vvalid g' v' -> vvalid g (vmap' v');
    evalid_bij: forall e, evalid g e -> evalid g' (emap e);
    evalid_bij_inv: forall e', evalid g' e' -> evalid g (emap' e');
    src_bij: forall e, evalid g e -> vmap (src g e) = src g' (emap e);
    dst_bij: forall e, evalid g e -> vmap (dst g e) = dst g' (emap e);
  }.

Lemma pregraph_iso_exp_refl: forall `(g: @PreGraph V E EV EE),
    pregraph_isomorphism_explicit g g id id id id.
Proof. intros. split; auto; apply bijective_refl. Qed.

Lemma pregraph_iso_exp_sym: forall
    `(g: @PreGraph V E EV EE) `(g': @PreGraph V' E' EV' EE') vmap vmap' emap emap',
    pregraph_isomorphism_explicit g g' vmap vmap' emap emap' ->
    pregraph_isomorphism_explicit g' g vmap' vmap emap' emap.
Proof.
  intros. destruct H. split; try assumption.
  - apply bijective_sym; assumption.
  - apply bijective_sym; assumption.
  - intros. destruct edge_bij0. apply evalid_bij_inv0 in H.
    rewrite <- (surjective e) at 1. rewrite <- src_bij0 by assumption.
    apply bijective_sym in vertex_bij0. destruct vertex_bij0.
    rewrite surjective0. reflexivity.
  - intros. destruct edge_bij0. apply evalid_bij_inv0 in H.
    rewrite <- (surjective e) at 1. rewrite <- dst_bij0 by assumption.
    apply bijective_sym in vertex_bij0. destruct vertex_bij0.
    rewrite surjective0. reflexivity.
Qed.

Lemma pregraph_iso_exp_trans: forall
    `(g1: @PreGraph V1 E1 EV1 EE1) `(g2: @PreGraph V2 E2 EV2 EE2)
    `(g3: @PreGraph V3 E3 EV3 EE3) v12 v21 e12 e21 v23 v32 e23 e32,
    pregraph_isomorphism_explicit g1 g2 v12 v21 e12 e21 ->
    pregraph_isomorphism_explicit g2 g3 v23 v32 e23 e32 ->
    pregraph_isomorphism_explicit g1 g3 (compose v23 v12) (compose v21 v32)
                                  (compose e23 e12) (compose e21 e32).
Proof.
  intros. destruct H, H0. split; intros; [| | unfold compose..]; auto.
  - eapply bijective_trans; auto.
  - eapply bijective_trans; auto.
  - rewrite <- src_bij1, <- src_bij0; auto.
  - rewrite <- dst_bij1, <- dst_bij0; auto.
Qed.

Local Coercion pg_lg: LabeledGraph >-> PreGraph.

Record label_preserving_graph_isomorphism_explicit
       `(g: @LabeledGraph V E EV EE DV DE DG) (g': @LabeledGraph V E EV EE DV DE DG)
       (vmap vmap': V -> V) (emap emap': E -> E): Prop :=
  {
    lp_pregraph_iso: pregraph_isomorphism_explicit g g' vmap vmap' emap emap';
    vlabel_iso: forall v, vvalid g v -> vlabel g v = vlabel g' (vmap v);
    elabel_iso: forall e, evalid g e -> elabel g e = elabel g' (emap e);
  }.

Lemma lp_graph_iso_exp_refl: forall `(g: @LabeledGraph V E EV EE DV DE DG),
    label_preserving_graph_isomorphism_explicit g g id id id id.
Proof. intros; split; auto. apply pregraph_iso_exp_refl. Qed.

Lemma lp_graph_iso_exp_sym: forall
    `(g: @LabeledGraph V E EV EE DV DE DG) g' vmap vmap' emap emap',
    label_preserving_graph_isomorphism_explicit g g' vmap vmap' emap emap' ->
    label_preserving_graph_isomorphism_explicit g' g vmap' vmap emap' emap.
Proof.
  intros. destruct H. split.
  - apply pregraph_iso_exp_sym. assumption.
  - intros. destruct lp_pregraph_iso0. destruct vertex_bij0.
    rewrite <- (surjective v) at 1. rewrite <- vlabel_iso0; auto.
  - intros. destruct lp_pregraph_iso0. destruct edge_bij0.
    rewrite <- (surjective e) at 1. rewrite <- elabel_iso0; auto.
Qed.

Lemma lp_graph_iso_exp_trans: forall
    `(g1: @LabeledGraph V E EV EE DV DE DG) g2 g3 v12 v21 e12 e21 v23 v32 e23 e32,
    label_preserving_graph_isomorphism_explicit g1 g2 v12 v21 e12 e21 ->
    label_preserving_graph_isomorphism_explicit g2 g3 v23 v32 e23 e32 ->
    label_preserving_graph_isomorphism_explicit
      g1 g3 (compose v23 v12) (compose v21 v32) (compose e23 e12) (compose e21 e32).
Proof.
  intros. destruct H, H0. split; intros; [|unfold compose..].
  - eapply pregraph_iso_exp_trans; eauto.
  - destruct lp_pregraph_iso0. rewrite vlabel_iso0, vlabel_iso1; auto.
  - destruct lp_pregraph_iso0. rewrite elabel_iso0, elabel_iso1; auto.
Qed.

Definition label_preserving_graph_isomorphism
           `(g: @LabeledGraph V E EV EE DV DE DG) g': Prop :=
  exists vmap vmap' emap emap',
    label_preserving_graph_isomorphism_explicit g g' vmap vmap' emap emap'.

Lemma lp_graph_iso_refl: forall `(g: @LabeledGraph V E EV EE DV DE DG),
    label_preserving_graph_isomorphism g g.
Proof. intros. exists id, id, id, id. apply lp_graph_iso_exp_refl. Qed.

Lemma lp_graph_iso_syn: forall `(g: @LabeledGraph V E EV EE DV DE DG) g',
    label_preserving_graph_isomorphism g g' -> label_preserving_graph_isomorphism g' g.
Proof.
  intros. destruct H as [vmap [vmap' [emap [emap' ?]]]].
  exists vmap', vmap, emap', emap. eapply lp_graph_iso_exp_sym; eauto.
Qed.

Lemma lp_graph_iso_trans: forall `(g1: @LabeledGraph V E EV EE DV DE DG) g2 g3,
    label_preserving_graph_isomorphism g1 g2 ->
    label_preserving_graph_isomorphism g2 g3 ->
    label_preserving_graph_isomorphism g1 g3.
Proof.
  intros. destruct H as [v12 [v21 [e12 [e21 ?]]]].
  destruct H0 as [v23 [v32 [e23 [e32 ?]]]].
  exists (compose v23 v12), (compose v21 v32), (compose e23 e12), (compose e21 e32).
  eapply lp_graph_iso_exp_trans; eauto.
Qed.

author: CertiGraph

repo: CertiGraph

save_path: github-repos/coq/CertiGraph-CertiGraph


text:
Require Import Iron.Data.Context.
Require Import Iron.Data.List.
Require Import Iron.Tactics.
Require Import Iron.Norm.

(* Chain of evaluation contexts.
   This carries the evaluation contexts needed to reduce
   a list of expressions in left-to-right order.

   Given a list of expressions:
     xs = [x1 x2 x3 x4 x5 x6 x7 x8]
   We want to prove that if each one is either a value or can be reduced
   to one, then we can evaluate the whole list of expressions to a list
   of values.
     vs = [v1 v2 v3 v4 v5 v6 v7 v8]
   To do this we need a list of evaluation contexts like follows,
   where XX is the expression currently being evaluated.
     C0:  [XX x1 x2 x3 x4 x5 x6 x7]
     C1:  [v0 XX x2 x3 x4 x5 x6 x7]
     C2:  [v0 v1 XX x3 x4 x5 x6 x7]
     C3:  [v0 v1 v2 XX x4 x5 x6 x7]
           ...
     C7:  [v0 v1 v2 v3 v4 v5 v6 XX ]
   The proof using these contexts proceeds *backwards* over
   the number of expressions that are known to be values.
   1) If all expressions are values then we're already done.
   2) For some context C, if we can reduce (C v) to all values,
      and we can reduce x to v, then we can also reduce (C x) to
      all values. This reasoning is similar to that used by the
      eval_expansion lemma.
   3) Producing the base-level context (C0) is trivial. We don't
      need to show that expressions to the left are already values,
      because there aren't any.
*)
Section Chain.
Variable exp       : Type.
Variable Val       : exp -> Prop.
Variable Steps     : exp -> exp -> Prop.
Variable Steps_val : forall x1 x2, Val x1 -> Steps x1 x2 -> x2 = x1.

Inductive CHAIN : list exp -> list exp -> Prop :=
 | EcDone
   :  forall vs
   ,  Forall Val vs
   -> CHAIN vs vs

 | EcCons
   :  forall x v vs C
   ,  exps_ctx Val C
   -> Steps x v -> Val v
   -> CHAIN (C v) vs
   -> CHAIN (C x) vs.
Hint Constructors CHAIN.

(* Add an already-evaluated expression to a chain.
   This effectively indicates that the expression was pre-evaluated
   and doesn't need to be evaluated again during the reduction. *)
Lemma chain_extend
 :  forall v xs ys
 ,  Val v
 -> CHAIN xs ys
 -> CHAIN (v :: xs) (v :: ys).
Proof.
 intros v xs ys HW HC.
 induction HC; auto.
  lets D1: (@XscCons exp) Val v H. auto.
  lets D2: EcCons D1 H0 H1 IHHC. auto.
Qed.

(* Make the chain of evaluation contexts needed to evaluate
   some expressions to values *)
Lemma make_chain
 :  forall xs vs
 ,  Forall2 Steps xs vs
 -> Forall  Val   vs
 -> CHAIN xs vs.
Proof.
 intros. gen vs.
 induction xs as [xs | x]; intros.
  Case "xs = nil".
   inverts H. auto.

  Case "xs = xs' :> v".
   destruct vs as [vs | v].

   SCase "vs = nil".
    nope.

   SCase "vs = vs' :> v".
    inverts H.
    inverts H0.
    have (CHAIN xs vs). clear IHxs.

    (* Build the property of STEPS we want to ass to exps_ctx2_run *)
    assert (Forall2
     (fun x v => Steps x v /\ Val v /\ (Val x -> v = x)) xs vs) as HS.
     eapply (@Forall2_impl_in exp exp Steps); auto.
      intros. nforall. rip.

    (* Either all the xs are already whnfX,
       or there is a context where one can step *)
    lets HR: (@exps_ctx2_run exp) Val HS. clear HS.
    inverts HR.

    SSCase "xs all whnfX".
     assert (Forall2 eq xs vs).
      eapply (@Forall2_impl_in exp exp Steps (@eq exp) xs vs).
      nforall. intros. symmetry. eauto. auto.

     assert (xs = vs).
      apply Forall2_eq. auto. subst.

     lets C1: (@XscHead exp) vs.
     lets D1: EcCons x v (v :: vs) C1 H4.
     eauto.

    SSCase "something steps".
     (* unpack the evaluation contexts *)
     dest C1. dest C2.
     destruct H0 as [x'].
     destruct H0 as [v'].
     rip.

     lets HC1: exps_ctx2_left  H0.
     lets HC2: exps_ctx2_right H0.

     assert (Val v').
      eapply exps_ctx_Forall; eauto.

     lets E1: (@XscCons exp) C1 H2 HC1.
     lets E2: (@XscCons exp) C2 H2 HC2.

   lets E3: (@XscHead exp) (C1 x').

   lets F1: EcCons x v (v :: C2 v') E3.
   apply F1; auto. clear F1.

   eapply chain_extend; auto.
Qed.

End Chain.

author: DonaldKellett

repo: iron-lambda


text:
(* Flat Combiner *)
From iris.algebra Require Import auth frac agree excl agree gset gmap.
From iris.base_logic Require Import saved_prop invariants.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang.lib Require Import spin_lock.
From iris_examples.logatom.flat_combiner Require Import misc peritem sync.
From iris.prelude Require Import options.

Set Default Proof Using "Type*".

Definition doOp : val :=
  λ: "p",
     match: !"p" with
       InjL "req" => "p" <- InjR ((Fst "req") (Snd "req"))
     | InjR "_" => #()
     end.

Definition try_srv : val :=
  λ: "lk" "s",
    if: try_acquire "lk"
      then let: "hd" := !"s" in
           treiber.iter "hd" doOp;;
           release "lk"
      else #().

Definition loop: val :=
  rec: "loop" "p" "s" "lk" :=
    match: !"p" with
    InjL "_" =>
        try_srv "lk" "s";;
        "loop" "p" "s" "lk"
    | InjR "r" => "r"
    end.

Definition install : val :=
  λ: "f" "x" "s",
     let: "p" := ref (InjL ("f", "x")) in
     push "s" "p";;
     "p".

Definition mk_flat : val :=
  λ: <>,
   let: "lk" := newlock #() in
   let: "s" := new_stack #() in
   λ: "f" "x",
      let: "p" := install "f" "x" "s" in
      let: "r" := loop "p" "s" "lk" in
      "r".

Definition reqR := prodR fracR (agreeR valO). (* request x should be kept same *)
Definition toks : Type := gname * gname * gname * gname * gname. (* a bunch of tokens to do state transition *)
Class flatG Σ := FlatG {
  req_G :> inG Σ reqR;
  sp_G  :> savedPredG Σ val
}.

Definition flatΣ : gFunctors :=
  #[ GFunctor (constRF reqR);
     savedPredΣ val ].

Global Instance subG_flatΣ {Σ} : subG flatΣ Σ → flatG Σ.
Proof. solve_inG. Qed.

Section proof.
  Context `{!heapGS Σ, !lockG Σ, !flatG Σ} (N: namespace).

  Definition init_s (ts: toks) :=
    let '(_, γ1, γ3, _, _) := ts in (own γ1 (Excl ()) ∗ own γ3 (Excl ()))%I.

  Definition installed_s R (ts: toks) (f x: val) :=
    let '(γx, γ1, _, γ4, γq) := ts in
    (∃ (P: val → iProp Σ) Q,
       own γx ((1/2)%Qp, to_agree x) ∗ P x ∗ ({{{ R ∗ P x }}} f x {{{ v, RET v; R ∗ Q x v }}}) ∗
       saved_pred_own γq (Q x) ∗ own γ1 (Excl ()) ∗ own γ4 (Excl ()))%I.

  Definition received_s (ts: toks) (x: val) γr :=
    let '(γx, _, _, γ4, _) := ts in
    (own γx ((1/2/2)%Qp, to_agree x) ∗ own γr (Excl ()) ∗ own γ4 (Excl ()))%I.

  Definition finished_s (ts: toks) (x y: val) :=
    let '(γx, γ1, _, γ4, γq) := ts in
    (∃ Q: val → val → iProp Σ,
       own γx ((1/2)%Qp, to_agree x) ∗ saved_pred_own γq (Q x) ∗
       Q x y ∗ own γ1 (Excl ()) ∗ own γ4 (Excl ()))%I.

  Definition p_inv R (γm γr: gname) (ts: toks) (p : loc) :=
    ( (* INIT *)
      (∃ y: val, p ↦ InjRV y ∗ init_s ts) ∨
      (* INSTALLED *)
      (∃ f x: val, p ↦ InjLV (f, x) ∗ installed_s R ts f x) ∨
      (* RECEIVED *)
      (∃ f x: val, p ↦ InjLV (f, x) ∗ received_s ts x γr) ∨
      (* FINISHED *)
      (∃ x y: val, p ↦ InjRV y ∗ finished_s ts x y))%I.

  Definition p_inv' R γm γr : val → iProp Σ :=
    (λ v: val, ∃ ts (p: loc), ⌜v = #p⌝ ∗ inv N (p_inv R γm γr ts p))%I.

  Definition srv_bag R γm γr s := (∃ xs, is_bag_R N (p_inv' R γm γr) xs s)%I.

  Definition installed_recp (ts: toks) (x: val) (Q: val → iProp Σ) :=
    let '(γx, _, γ3, _, γq) := ts in
    (own γ3 (Excl ()) ∗ own γx ((1/2)%Qp, to_agree x) ∗ saved_pred_own γq Q)%I.

  Lemma install_spec R P Q (f x: val) (γm γr: gname) (s: loc):
    {{{ inv N (srv_bag R γm γr s) ∗ P ∗ ({{{ R ∗ P }}} f x {{{ v, RET v; R ∗ Q v }}}) }}}
      install f x #s
    {{{ p ts, RET #p; installed_recp ts x Q ∗ inv N (p_inv R γm γr ts p) }}}.
  Proof.
    iIntros (Φ) "(#? & HP & Hf) HΦ".
    wp_lam. wp_pures. wp_alloc p as "Hl".
    iApply fupd_wp.
    iMod (own_alloc (Excl ())) as (γ1) "Ho1"; first done.
    iMod (own_alloc (Excl ())) as (γ3) "Ho3"; first done.
    iMod (own_alloc (Excl ())) as (γ4) "Ho4"; first done.
    iMod (own_alloc (1%Qp, to_agree x)) as (γx) "Hx"; first done.
    iMod (saved_pred_alloc Q) as (γq) "#?".
    iDestruct (own_update with "Hx") as ">[Hx1 Hx2]"; first by apply pair_l_frac_op_1'.
    iModIntro. wp_let. wp_bind (push _ _).
    iMod (inv_alloc N _ (p_inv R γm γr (γx, γ1, γ3, γ4, γq) p)
          with "[-HΦ Hx2 Ho3]") as "#HRx"; first eauto.
    { iNext. iRight. iLeft. iExists f, x. iFrame.
      iExists (λ _, P), (λ _ v, Q v).
      iFrame. iFrame "#". }
    iApply (push_spec N (p_inv' R γm γr) s #p
            with "[-HΦ Hx2 Ho3]")=>//.
    { iFrame "#". iExists (γx, γ1, γ3, γ4, γq), p.
      iSplitR; first done. iFrame "#". }
    iNext. iIntros "?".
    wp_seq. iApply ("HΦ" $! p (γx, γ1, γ3, γ4, γq)).
    iFrame. by iFrame "#".
  Qed.

  Lemma doOp_f_spec R γm γr (p: loc) ts:
    f_spec N (p_inv R γm γr ts p) doOp (own γr (Excl ()) ∗ R)%I #p.
  Proof.
    iIntros (Φ) "(#H1 & Hor & HR) HΦ".
    wp_rec. wp_bind (! _)%E.
    iInv N as "Hp" "Hclose".
    iDestruct "Hp" as "[Hp | [Hp | [Hp | Hp]]]"; subst.
    - iDestruct "Hp" as (y) "[>Hp Hts]".
      wp_load. iMod ("Hclose" with "[-Hor HR HΦ]").
      { iNext. iFrame "#". iLeft. iExists y. iFrame. }
      iModIntro. wp_match. iApply ("HΦ" with "[Hor HR]"). iFrame.
    - destruct ts as [[[[γx γ1] γ3] γ4] γq].
      iDestruct "Hp" as (f x) "(>Hp & Hts)".
      iDestruct "Hts" as (P Q) "(>Hx & Hpx & Hf' & HoQ & >Ho1 & >Ho4)".
      iAssert (|==> own γx (((1/2/2)%Qp, to_agree x) ⋅
                            ((1/2/2)%Qp, to_agree x)))%I with "[Hx]" as ">[Hx1 Hx2]".
      { iDestruct (own_update with "Hx") as "?"; last by iAssumption.
        rewrite -{1}(Qp_div_2 (1/2)%Qp).
        by apply pair_l_frac_op'. }
      wp_load. iMod ("Hclose" with "[-Hf' Ho1 Hx2 HoQ HR HΦ Hpx]") as "_".
      { iNext. rewrite {2}/p_inv. iRight. iRight. iLeft. iExists f, x. iFrame. }
      iModIntro. wp_match. wp_pures.
      wp_bind (f _). iApply ("Hf'" with "[$HR $Hpx]").
      iIntros "!>" (v) "[HR HQ]". wp_pures.
      iInv N as "Hx" "Hclose".
      iDestruct "Hx" as "[Hp | [Hp | [Hp | Hp]]]"; subst.
      * iDestruct "Hp" as (?) "(_ & >Ho1' & _)".
        iApply excl_falso. iFrame.
      * iDestruct "Hp" as (? ?) "[>? Hs]". iDestruct "Hs" as (? ?) "(_ & _ & _ & _ & >Ho1' & _)".
        iApply excl_falso. iFrame.
      * iDestruct "Hp" as (? x5) ">(Hp & Hx & Hor & Ho4)".
        wp_store. iDestruct (m_frag_agree' with "Hx Hx2") as "[Hx %]".
        subst. rewrite Qp_div_2. iMod ("Hclose" with "[-HR Hor HΦ]").
        { iNext. iDestruct "Hp" as "[Hp1 Hp2]". iRight. iRight.
          iRight. iExists _, v. iFrame. iExists Q. iFrame. }
        iApply "HΦ". iFrame. done.
      * iDestruct "Hp" as (? ?) "[? Hs]". iDestruct "Hs" as (?) "(_ & _ & _ & >Ho1' & _)".
        iApply excl_falso. iFrame.
    - destruct ts as [[[[γx γ1] γ3] γ4] γq]. iDestruct "Hp" as (? x) "(_ & _ & >Ho2' & _)".
      iApply excl_falso. iFrame.
    - destruct ts as [[[[γx γ1] γ3] γ4] γq]. iDestruct "Hp" as (x' y) "[Hp Hs]".
        iDestruct "Hs" as (Q) "(>Hx & HoQ & HQxy & >Ho1 & >Ho4)".
        wp_load. iMod ("Hclose" with "[-HΦ HR Hor]").
        { iNext. iRight. iRight. iRight. iExists x', y. iFrame. iExists Q. iFrame. }
        iModIntro. wp_match. iApply "HΦ". by iFrame.
  Qed.

  Definition own_γ3 (ts: toks) := let '(_, _, γ3, _, _) := ts in own γ3 (Excl ()).
  Definition finished_recp (ts: toks) (x y: val) :=
    let '(γx, _, _, _, γq) := ts in
    (∃ Q, own γx ((1 / 2)%Qp, to_agree x) ∗ saved_pred_own γq (Q x) ∗ Q x y)%I.

  Lemma loop_iter_doOp_spec R (γm γr: gname) xs:
  ∀ (hd: loc),
    {{{ is_list_R N (p_inv' R γm γr) hd xs ∗ own γr (Excl ()) ∗ R }}}
      treiber.iter #hd doOp
    {{{ RET #(); own γr (Excl ()) ∗ R }}}.
  Proof.
    induction xs as [|x xs' IHxs].
    - iIntros (hd Φ) "[Hxs ?] HΦ".
      simpl. wp_rec. wp_let.
      wp_load. wp_match. by iApply "HΦ".
    - iIntros (hd Φ) "[Hxs HRf] HΦ". simpl.
      iDestruct "Hxs" as (hd') "(#Hhd & #Hinv & Hxs')".
      wp_rec. wp_let. wp_bind (! _)%E.
      iInv N as "H" "Hclose".
      iDestruct "H" as (ts p) "[>% #?]". subst.
      wp_load. iMod ("Hclose" with "[]").
      { iNext. iExists ts, p. eauto. }
      iModIntro. wp_match. wp_proj. wp_bind (doOp _).
      iDestruct (doOp_f_spec R γm γr p ts) as "Hf".
      iApply ("Hf" with "[HRf]").
      { iFrame. iFrame "#". }
      iNext. iIntros "HRf".
      wp_seq. wp_proj. iApply (IHxs with "[-HΦ]")=>//.
      iFrame "#"; first by iFrame.
  Qed.

  Lemma try_srv_spec R (s: loc) (lk: val) (γr γm γlk: gname) Φ :
    inv N (srv_bag R γm γr s) ∗
    is_lock γlk lk (own γr (Excl ()) ∗ R) ∗ Φ #()
    ⊢ WP try_srv lk #s {{ Φ }}.
  Proof.
    iIntros "(#? & #? & HΦ)". wp_lam. wp_pures.
    wp_bind (try_acquire _). iApply (try_acquire_spec with "[]"); first done.
    iNext. iIntros ([]); last by (iIntros; wp_if).
    iIntros "[Hlocked [Ho2 HR]]".
    wp_if. wp_bind (! _)%E.
    iInv N as "H" "Hclose".
    iDestruct "H" as (xs' hd') "[>Hs #Hxs]".
    wp_load.
    iMod ("Hclose" with "[Hs]").
    { iNext. iFrame. iExists xs', hd'. by iFrame. }
    iModIntro. wp_let. wp_bind (treiber.iter _ _).
    iApply wp_wand_r. iSplitL "HR Ho2".
    { iApply (loop_iter_doOp_spec R _ _ _ _ (λ _, own γr (Excl ()) ∗ R)%I with "[-]")=>//.
      - iFrame "#∗".
      - eauto. }
    iIntros (f') "[Ho HR]". wp_seq.
    iApply (release_spec with "[Hlocked Ho HR]"); first iFrame "#∗".
    iNext. iIntros. done.
  Qed.

  Lemma loop_spec R (p s: loc) (lk: val)
        (γs γr γm γlk: gname) (ts: toks):
    {{{ inv N (srv_bag R γm γr s) ∗ inv N (p_inv R γm γr ts p) ∗
        is_lock γlk lk (own γr (Excl ()) ∗ R) ∗ own_γ3 ts }}}
      loop #p #s lk
    {{{ x y, RET y; finished_recp ts x y }}}.
  Proof.
    iIntros (Φ) "(#? & #? & #? & Ho3) HΦ".
    iLöb as "IH". wp_rec. repeat wp_let.
    wp_bind (! _)%E. iInv N as "Hp" "Hclose".
    destruct ts as [[[[γx γ1] γ3] γ4] γq].
    iDestruct "Hp" as "[Hp | [Hp | [ Hp | Hp]]]".
    + iDestruct "Hp" as (?) "(_ & _ & >Ho3')".
      iApply excl_falso. iFrame.
    + iDestruct "Hp" as (f x) "(>Hp & Hs')".
      wp_load. iMod ("Hclose" with "[Hp Hs']").
      { iNext. iFrame. iRight. iLeft. iExists f, x. iFrame. }
      iModIntro. wp_match. wp_bind (try_srv _ _). iApply try_srv_spec=>//.
      iFrame "#". wp_seq. iApply ("IH" with "Ho3"); eauto.
    + iDestruct "Hp" as (f x) "(Hp & Hx & Ho2 & Ho4)".
      wp_load. iMod ("Hclose" with "[-Ho3 HΦ]") as "_".
      { iNext. (* FIXME: iFrame here divergses, with an enormous TC trace *)
        iRight. iRight. iLeft. iExists f, x. iFrame. }
      iModIntro. wp_match.
      wp_bind (try_srv _ _). iApply try_srv_spec=>//.
      iFrame "#". wp_seq. iApply ("IH" with "Ho3"); eauto.
    + iDestruct "Hp" as (x y) "[>Hp Hs']".
      iDestruct "Hs'" as (Q) "(>Hx & HoQ & HQ & >Ho1 & >Ho4)".
      wp_load. iMod ("Hclose" with "[-Ho4 HΦ Hx HoQ HQ]").
      { iNext. iLeft. iExists y. iFrame. }
      iModIntro. wp_match. iApply ("HΦ" with "[-]"). iFrame.
      iExists Q. iFrame.
  Qed.

  Lemma mk_flat_spec (γm: gname): mk_syncer_spec mk_flat.
  Proof using Type* N.
    iIntros (R Φ) "HR HΦ".
    iMod (own_alloc (Excl ())) as (γr) "Ho2"; first done.
    wp_lam. wp_bind (newlock _).
    iApply (newlock_spec (own γr (Excl ()) ∗ R)%I with "[$Ho2 $HR]")=>//.
    iNext. iIntros (lk γlk) "#Hlk".
    wp_let. wp_bind (new_stack _).
    iApply (new_bag_spec N (p_inv' R γm γr))=>//.
    iNext. iIntros (s) "#Hss".
    wp_pures. iModIntro. iApply "HΦ".
    iModIntro. iIntros (f). wp_pures.
    iIntros "!> !>" (P Q x) "#Hf !>".
    iIntros (Φ') "Hp HΦ'". wp_pures. wp_bind (install _ _ _).
    iApply (install_spec R P Q f x γm γr s with "[Hp]")=>//.
    { iFrame. iFrame "#". }
    iNext. iIntros (p [[[[γx γ1] γ3] γ4] γq]) "[(Ho3 & Hx & HoQ) #?]".
    wp_let. wp_bind (loop _ _ _).
    iApply (loop_spec with "[-Hx HoQ HΦ']")=>//.
    { iFrame "#". iFrame. }
    iNext. iIntros (v1 v2) "Hs".
    iDestruct "Hs" as (Q') "(Hx' & HoQ' & HQ')".
    destruct (decide (x = v1)) as [->|Hneq].
    - iDestruct (saved_pred_agree _ _ _ v2 with "[$HoQ] [HoQ']") as "Heq"; first by iFrame.
      wp_let. iApply "HΦ'". by iRewrite -"Heq" in "HQ'".
    - iExFalso. iCombine "Hx" "Hx'" as "Hx".
      iDestruct (own_valid with "Hx") as %[_ H1].
      rewrite //= in H1.
      by apply to_agree_op_inv in H1.
  Qed.

End proof.

author: pavel-ivanov-rnd

repo: iris-heaplang-experiments


text:
(* *********************************************************************)
(*                                                                     *)
(*              The Compcert verified compiler                         *)
(*                                                                     *)
(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
(*                                                                     *)
(*  Copyright Institut National de Recherche en Informatique et en     *)
(*  Automatique.  All rights reserved.  This file is distributed       *)
(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
(*                                                                     *)
(* *********************************************************************)

(** Typing rules for LTL. *)

Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Op.
Require Import Locations.
Require Import LTL.
Require Import Conventions.

(** The following predicates define a type system for LTL similar to that
  of [RTL] (see file [RTLtyping]): it statically guarantees that operations
  and addressing modes are applied to the right number of arguments
  and that the arguments are of the correct types.  Moreover, it also
  guarantees that the locations of arguments and results are "acceptable",
  i.e. either non-temporary registers or [Local] stack locations. *)

Section WITHEF.
Context `{Hsc: SyntaxConfiguration}.

Section WT_INSTR.

Variable funct: function.

Definition valid_successor (s: node) : Prop :=
  exists i, funct.(fn_code)!s = Some i.

Definition call_loc_acceptable (sig: signature) (los: loc + ident) : Prop :=
  match los with
  | inl l => Loc.type l = Tint /\ loc_acceptable l /\ ~In l (loc_arguments sig)
  | inr s => True
  end.

Inductive wt_instr : instruction -> Prop :=
  | wt_Lnop:
      forall s,
      valid_successor s ->
      wt_instr (Lnop s)
  | wt_Lopmove:
      forall r1 r s,
      Loc.type r1 = Loc.type r -> loc_acceptable r1 -> loc_acceptable r ->
      valid_successor s ->
      wt_instr (Lop Omove (r1 :: nil) r s)
  | wt_Lop:
      forall op args res s,
      op <> Omove ->
      (List.map Loc.type args, Loc.type res) = type_of_operation op ->
      locs_acceptable args -> loc_acceptable res ->
      valid_successor s ->
      wt_instr (Lop op args res s)
  | wt_Lload:
      forall chunk addr args dst s,
      List.map Loc.type args = type_of_addressing addr ->
      Loc.type dst = type_of_chunk chunk ->
      locs_acceptable args -> loc_acceptable dst ->
      valid_successor s ->
      wt_instr (Lload chunk addr args dst s)
  | wt_Lstore:
      forall chunk addr args src s,
      List.map Loc.type args = type_of_addressing addr ->
      Loc.type src = type_of_chunk chunk ->
      locs_acceptable args -> loc_acceptable src ->
      valid_successor s ->
      wt_instr (Lstore chunk addr args src s)
  | wt_Lcall:
      forall sig ros args res s,
      List.map Loc.type args = sig.(sig_args) ->
      Loc.type res = proj_sig_res sig ->
      call_loc_acceptable sig ros ->
      locs_acceptable args -> loc_acceptable res ->
      valid_successor s ->
      wt_instr (Lcall sig ros args res s)
  | wt_Ltailcall:
      forall sig ros args,
      List.map Loc.type args = sig.(sig_args) ->
      call_loc_acceptable sig ros ->
      locs_acceptable args ->
      sig.(sig_res) = funct.(fn_sig).(sig_res) ->
      tailcall_possible sig ->
      wt_instr (Ltailcall sig ros args)
  | wt_Lbuiltin:
      forall ef args res s,
      List.map Loc.type args = (ef_sig ef).(sig_args) ->
      Loc.type res = proj_sig_res (ef_sig ef) ->
      arity_ok (ef_sig ef).(sig_args) = true \/ ef_reloads ef = false ->
      locs_acceptable args -> loc_acceptable res ->
      valid_successor s ->
      wt_instr (Lbuiltin ef args res s)
  | wt_Lcond:
      forall cond args s1 s2,
      List.map Loc.type args = type_of_condition cond ->
      locs_acceptable args ->
      valid_successor s1 -> valid_successor s2 ->
      wt_instr (Lcond cond args s1 s2)
  | wt_Ljumptable:
      forall arg tbl,
      Loc.type arg = Tint ->
      loc_acceptable arg ->
      (forall lbl, In lbl tbl -> valid_successor lbl) ->
      list_length_z tbl * 4 <= Int.max_unsigned ->
      wt_instr (Ljumptable arg tbl)
  | wt_Lreturn:
      forall optres,
      option_map Loc.type optres = funct.(fn_sig).(sig_res) ->
      match optres with None => True | Some r => loc_acceptable r end ->
      wt_instr (Lreturn optres).

End WT_INSTR.

Record wt_function (f: function): Prop :=
  mk_wt_function {
    wt_params:
      List.map Loc.type f.(fn_params) = f.(fn_sig).(sig_args);
    wt_acceptable:
      locs_acceptable f.(fn_params);
    wt_norepet:
      Loc.norepet f.(fn_params);
    wt_instrs:
      forall pc instr,
      f.(fn_code)!pc = Some instr -> wt_instr f instr;
    wt_entrypoint:
      valid_successor f f.(fn_entrypoint)
}.

Inductive wt_fundef: fundef -> Prop :=
  | wt_fundef_external: forall ef,
      wt_fundef (External ef)
  | wt_function_internal: forall f,
      wt_function f ->
      wt_fundef (Internal f).

Definition wt_program (p: program): Prop :=
  forall i f, In (i, Gfun f) (prog_defs p) -> wt_fundef f.

End WITHEF.

author: jeremie-koenig

repo: compcert


text:
(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div fintype path.
Require Import finset prime fingroup automorphism action gproduct gfunctor.
Require Import center commutator pgroup gseries nilpotent sylow abelian maximal.
Require Import BGsection1 BGsection5 BGsection6 BGsection7.

(******************************************************************************)
(*   This file covers B & G, section 8, i.e., the proof of two special cases  *)
(* of the Uniqueness Theorem, for maximal groups with Fitting subgroups of    *)
(* rank at least 3.                                                           *)
(******************************************************************************)

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

Import GroupScope.

Section Eight.

Variable gT : minSimpleOddGroupType.
Local Notation G := (TheMinSimpleOddGroup gT).
Implicit Types H M A X P : {group gT}.
Implicit Types p q r : nat.

Local Notation "K ` p" := 'O_(nat_pred_of_nat p)(K)
  (at level 8, p at level 2, format "K ` p") : group_scope.
Local Notation "K ` p" := 'O_(nat_pred_of_nat p)(K)%G : Group_scope.

(* This is B & G, Theorem 8.1(a). *)
Theorem non_pcore_Fitting_Uniqueness p M A0 :
    M \in 'M -> ~~ p.-group ('F(M)) -> A0 \in 'E*_p('F(M)) -> 'r_p(A0) >= 3 ->
  'C_('F(M))(A0)%G \in 'U.
Proof.
set F := 'F(M) => maxM p'F /pmaxElemP[/=/setIdP[sA0F abelA0] maxA0].
have [pA0 cA0A0 _] := and3P abelA0; rewrite (p_rank_abelem abelA0) => dimA0_3.
rewrite (uniq_mmax_subset1 maxM) //= -/F; last by rewrite subIset ?Fitting_sub.
set A := 'C_F(A0); pose pi := \pi(A).
have [sZA sAF]: 'Z(F) \subset A /\ A \subset F by rewrite subsetIl setIS ?centS.
have nilF: nilpotent F := Fitting_nil _.
have nilZ := nilpotentS (center_sub _) nilF.
have piZ: \pi('Z(F)) = \pi(F) by rewrite pi_center_nilpotent.
have def_pi: pi = \pi(F).
  by apply/eq_piP=> q; apply/idP/idP; last rewrite -piZ; apply: piSg.
have def_nZq: forall q, q \in pi -> 'N('Z(F)`q) = M.
  move=> q; rewrite def_pi -piZ -p_part_gt1.
  rewrite -(card_Hall (nilpotent_pcore_Hall _ nilZ)) cardG_gt1 /= -/F => ntZ.
  by apply: mmax_normal => //=; rewrite !gFnormal_trans.
have sCqM: forall q, q \in pi -> 'C(A`q) \subset M.
  move=> q /def_nZq <-; rewrite cents_norm // centS //.
  rewrite (sub_Hall_pcore (nilpotent_pcore_Hall _ _)) ?pcore_pgroup //.
    by apply: nilpotentS (Fitting_nil M); apply: subsetIl.
  exact: gFsub_trans.
have sA0A: A0 \subset A by rewrite subsetI sA0F.
have pi_p: p \in pi.
  by apply: (piSg sA0A); rewrite -[p \in _]logn_gt0 (leq_trans _ dimA0_3).
have sCAM: 'C(A) \subset M.
  by rewrite (subset_trans (centS (pcore_sub p _))) ?sCqM.
have prM: M \proper G := mmax_proper maxM; have solM := mFT_sol prM.
have piCA: pi.-group('C(A)).
  apply/pgroupP=> q q_pr; case/Cauchy=> // x cAx oxq; apply/idPn=> pi'q.
  have Mx := subsetP sCAM x cAx; pose C := 'C_F(<[x]>).
  have sAC: A \subset C by rewrite subsetI sAF centsC cycle_subG.
  have sCFC_C: 'C_F(C) \subset C.
    by rewrite (subset_trans _ sAC) ?setIS // centS ?(subset_trans _ sAC).
  have cFx: x \in 'C_M(F).
    rewrite inE Mx -cycle_subG coprime_nil_faithful_cent_stab //=.
      by rewrite cycle_subG (subsetP (gFnorm _ _)).
    by rewrite -orderE coprime_pi' ?cardG_gt0 // -def_pi oxq pnatE.
  case/negP: pi'q; rewrite def_pi mem_primes q_pr cardG_gt0 -oxq cardSg //.
  by rewrite cycle_subG (subsetP (cent_sub_Fitting _)).
have{p'F} pi_alt q: exists2 r, r \in pi & r != q.
  have [<-{q} | ] := eqVneq p q; last by exists p.
  rewrite def_pi; apply/allPn; apply: contra p'F => /allP/=pF.
  by apply/pgroupP=> q q_pr qF; rewrite !inE pF // mem_primes q_pr cardG_gt0.
have sNZqXq' q X:
  A \subset X -> X \proper G -> 'O_q^'('N_X('Z(F)`q)) \subset 'O_q^'(X).
- move=> sAX prX.
  have sZqX: 'Z(F)`q \subset X by apply: gFsub_trans (subset_trans sZA sAX).
  have cZqNXZ: 'O_q^'('N_X('Z(F)`q)) \subset 'C('Z(F)`q).
    have coNq'Zq: coprime #|'O_q^'('N_X('Z(F)`q))| #|'Z(F)`q|.
      by rewrite coprime_sym coprime_pcoreC.
    rewrite (sameP commG1P trivgP) -(coprime_TIg coNq'Zq) subsetI commg_subl /=.
    rewrite commg_subr /= andbC gFsub_trans ?subsetIr //=.
    by rewrite gFnorm_trans ?normsG // subsetI sZqX normG.
  have: 'O_q^'('C_X(('Z(F))`q)) \subset 'O_q^'(X).
    by rewrite p'core_cent_pgroup ?mFT_sol // /psubgroup sZqX pcore_pgroup.
  apply: subset_trans; apply: subset_trans (pcoreS _ (subcent_sub _ _)).
  by rewrite !subsetI subxx cZqNXZ gFsub_trans ?subsetIl.
have sArXq' q r X:
  q \in pi -> q != r -> A \subset X -> X \proper G -> A`r \subset 'O_q^'(X).
- move=> pi_q r'q sAX prX; apply: subset_trans (sNZqXq' q X sAX prX).
  apply: subset_trans (pcoreS _ (subsetIr _ _)).
  rewrite -setIA (setIidPr (pcore_sub _ _)) subsetI gFsub_trans //= def_nZq //.
  apply: subset_trans (pcore_Fitting _ _); rewrite -/F.
  rewrite (sub_Hall_pcore (nilpotent_pcore_Hall _ nilF)) ?gFsub_trans //.
  by apply: (pi_pnat (pcore_pgroup _ _)); rewrite !inE eq_sym.
have cstrA: normed_constrained A.
  split=> [||X Y sAX prX].
  - by apply/eqP=> A1; rewrite /pi /= A1 cards1 in pi_p.
  - exact: sub_proper_trans (subset_trans sAF (Fitting_sub _)) prM.
  rewrite !inE -/pi -andbA => /and3P[sYX pi'Y nYA].
  rewrite -bigcap_p'core subsetI sYX; apply/bigcapsP=> [[q /= _] pi_q].
  have [r pi_r q'r] := pi_alt q.
  have{sArXq'} sArXq': A`r \subset 'O_q^'(X) by apply: sArXq'; rewrite 1?eq_sym.
  have cA_CYr: 'C_Y(A`r) \subset 'C(A).
    have coYF: coprime #|Y| #|F|.
      by rewrite coprime_sym coprime_pi' ?cardG_gt0 // -def_pi.
    rewrite (sameP commG1P trivgP) -(coprime_TIg coYF) commg_subI //.
      by rewrite setIS // (subset_trans (sCqM r pi_r)) // gFnorm.
    by rewrite subsetI subsetIl.
  have{cA_CYr} CYr1: 'C_Y(A`r) = 1.
    rewrite -(setIid Y) setIAC coprime_TIg // (coprimeSg cA_CYr) //.
    by rewrite (pnat_coprime piCA).
  have{CYr1} ->: Y :=: [~: Y, A`r].
    rewrite -(mulg1 [~: Y, _]) -CYr1 coprime_cent_prod ?gFsub_trans //.
      rewrite coprime_sym (coprimeSg (pcore_sub _ _)) //= -/A.
      by rewrite coprime_pi' ?cardG_gt0.
    by rewrite mFT_sol // (sub_proper_trans sYX).
  rewrite (subset_trans (commgS _ sArXq')) //.
  by rewrite commg_subr gFnorm_trans ?normsG.
have{cstrA} nbyApi'1 q: q \in pi^' -> |/|*(A; q) = [set 1%G].
  move=> pi'q; have trA: [transitive 'O_pi^'('C(A)), on |/|*(A; q) | 'JG].
    apply: normed_constrained_rank3_trans; rewrite //= -/A.
    rewrite -rank_abelem // in dimA0_3; apply: leq_trans dimA0_3 (rankS _).
    by rewrite /= -/A subsetI sA0A centsC subsetIr.
  have [Q maxQ defAmax]: exists2 Q, Q \in |/|*(A; q) & |/|*(A; q) = [set Q].
    case/imsetP: trA => Q maxQ defAmax; exists Q; rewrite // {maxQ}defAmax.
    suffices ->: 'O_pi^'('C(A)) = 1 by rewrite /orbit imset_set1 act1.
    rewrite -(setIidPr (pcore_sub _ _)) coprime_TIg //.
    exact: pnat_coprime piCA (pcore_pgroup _ _).
  have{maxQ} qQ: q.-group Q by move: maxQ; rewrite inE => /maxgroupp/andP[].
  have [<- // |] := eqVneq Q 1%G; rewrite -val_eqE /= => ntQ.
  have{defAmax trA} defFmax: |/|*(F; q) = [set Q].
    apply/eqP; rewrite eqEcard cards1 -defAmax.
    have snAF: A <|<| F by rewrite nilpotent_subnormal ?Fitting_nil.
    have piF: pi.-group F by rewrite def_pi /pgroup pnat_pi ?cardG_gt0.
    case/(normed_trans_superset _ _ snAF): trA => //= _ /imsetP[R maxR _] -> _.
    by rewrite (cardsD1 R) maxR.
  have nQM: M \subset 'N(Q).
    apply/normsP=> x Mx; apply: congr_group; apply/set1P.
    rewrite -defFmax (acts_act (norm_acts_max_norm _ _)) ?defFmax ?set11 //.
    by apply: subsetP Mx; apply: gFnorm.
  have{nQM} nsQM: Q <| M.
    rewrite inE in maxM; case/maxgroupP: maxM => _ maxM.
    rewrite -(maxM 'N(Q)%G) ?normalG ?mFT_norm_proper //.
    exact: mFT_pgroup_proper qQ.
  have sQF: Q \subset F by rewrite Fitting_max ?(pgroup_nil qQ).
  rewrite -(setIidPr sQF) coprime_TIg ?eqxx // in ntQ.
  by rewrite coprime_pi' ?cardG_gt0 // -def_pi (pi_pnat qQ).
apply/subsetP=> H /setIdP[maxH sAH]; rewrite inE -val_eqE /=.
have prH: H \proper G := mmax_proper maxH; have solH := mFT_sol prH.
pose D := 'F(H); have nilD: nilpotent D := Fitting_nil H.
have card_pcore_nil := card_Hall (nilpotent_pcore_Hall _ _).
have piD: \pi(D) = pi.
  set sigma := \pi(_); have pi_sig: {subset sigma <= pi}.
    move=> q; rewrite -p_part_gt1 -card_pcore_nil // cardG_gt1 /= -/D.
    apply: contraR => /nbyApi'1 defAmax.
    have nDqA: A \subset 'N(D`q).
      by rewrite gFnorm_trans // (subset_trans sAH) ?gFnorm.
    have [Q]:= max_normed_exists (pcore_pgroup _ _) nDqA.
    by rewrite defAmax -subG1; move/set1P->.
  apply/eq_piP=> q; apply/idP/idP=> [|pi_q]; first exact: pi_sig.
  apply: contraLR (pi_q) => sig'q; have nilA := nilpotentS sAF nilF.
  rewrite -p_part_eq1 -card_pcore_nil // -trivg_card1 -subG1 /= -/A.
  have <-: 'O_sigma^'(H) = 1.
    apply/eqP; rewrite -trivg_Fitting ?(solvableS (pcore_sub _ _)) //.
    rewrite Fitting_pcore -(setIidPr (pcore_sub _ _)) coprime_TIg //.
    by rewrite coprime_pi' ?cardG_gt0 //; apply: pcore_pgroup.
  rewrite -bigcap_p'core subsetI gFsub_trans //=.
  apply/bigcapsP=> -[r /= _] sig_r; apply: sArXq' => //; first exact: pi_sig.
  by apply: contraNneq sig'q => <-.
have cAD q r: q != r -> D`q \subset 'C(A`r).
  move=> r'q; have [-> |] := eqVneq D`q 1; first by rewrite sub1G.
  rewrite -cardG_gt1 card_pcore_nil // p_part_gt1 piD => pi_q.
  have sArHq': A`r \subset 'O_q^'(H) by rewrite sArXq'.
  have coHqHq': coprime #|D`q| #|'O_q^'(H)| by rewrite coprime_pcoreC.
  rewrite (sameP commG1P trivgP) -(coprime_TIg coHqHq') commg_subI //.
    by rewrite subsetI subxx /= p_core_Fitting gFsub_trans ?gFnorm.
  rewrite subsetI sArHq' gFsub_trans ?(subset_trans sAH) //=.
  by rewrite p_core_Fitting gFnorm.
have sDM: D \subset M.
  rewrite [D]FittingEgen gen_subG; apply/bigcupsP=> [[q /= _] _].
  rewrite -p_core_Fitting -/D; have [r pi_r r'q] := pi_alt q.
  by apply: subset_trans (sCqM r pi_r); apply: cAD; rewrite eq_sym.
have cApHp': A`p \subset 'C('O_p^'(H)).
  have coApHp': coprime #|'O_p^'(H)| #|A`p|.
    by rewrite coprime_sym coprime_pcoreC.
  have solHp': solvable 'O_p^'(H) by rewrite (solvableS (pcore_sub _ _)).
  have nHp'Ap: A`p \subset 'N('O_p^'(H)).
    by rewrite gFsub_trans ?gFnorm_trans ?normsG.
  apply: subset_trans (coprime_cent_Fitting nHp'Ap coApHp' solHp').
  rewrite subsetI subxx centsC /= FittingEgen gen_subG.
  apply/bigcupsP=> [[q /= _] _]; have [-> | /cAD] := eqVneq q p.
    by rewrite -(setIidPl (pcore_sub p _)) TI_pcoreC sub1G.
  apply: subset_trans; rewrite p_core_Fitting -pcoreI.
  by apply: sub_pcore => r /andP[].
have sHp'M: 'O_p^'(H) \subset M.
  by apply: subset_trans (sCqM p pi_p); rewrite centsC.
have ntDp: D`p != 1 by rewrite -cardG_gt1 card_pcore_nil // p_part_gt1 piD.
have sHp'_NMDp': 'O_p^'(H) \subset 'O_p^'('N_M(D`p)).
  apply: subset_trans (pcoreS _ (subsetIr _ _)).
  rewrite -setIA (setIidPr (pcore_sub _ _)) /= (mmax_normal maxH) //.
    by rewrite subsetI sHp'M subxx.
  by rewrite /= p_core_Fitting pcore_normal.
have{sHp'_NMDp'} sHp'Mp': 'O_p^'(H) \subset 'O_p^'(M).
  have pM_D: p.-subgroup(M) D`p.
    by rewrite /psubgroup pcore_pgroup gFsub_trans.
  apply: subset_trans (p'core_cent_pgroup pM_D (mFT_sol prM)).
  apply: subset_trans (pcoreS _ (subcent_sub _ _)).
  rewrite !subsetI sHp'_NMDp' sHp'M andbT /= (sameP commG1P trivgP).
  have coHp'Dp: coprime #|'O_p^'(H)| #|D`p|.
    by rewrite coprime_sym coprime_pcoreC.
  rewrite -(coprime_TIg coHp'Dp) subsetI commg_subl commg_subr /=.
  by rewrite p_core_Fitting !gFsub_trans ?gFnorm.
have sMp'H: 'O_p^'(M) \subset H.
  rewrite -(mmax_normal maxH (pcore_normal p H)) /= -p_core_Fitting //.
  rewrite -/D (subset_trans _ (cent_sub _)) // centsC.
  have solMp' := solvableS (pcore_sub p^' _) (mFT_sol prM).
  have coMp'Dp: coprime #|'O_p^'(M)| #|D`p|.
    by rewrite coprime_sym coprime_pcoreC.
  have nMp'Dp: D`p \subset 'N('O_p^'(M)).
    by rewrite gFsub_trans ?(subset_trans sDM) ?gFnorm.
  apply: subset_trans (coprime_cent_Fitting nMp'Dp coMp'Dp solMp').
  rewrite subsetI subxx centsC /= FittingEgen gen_subG.
  apply/bigcupsP=> [[q /= _] _]; have [<- | /cAD] := eqVneq p q.
    by rewrite -(setIidPl (pcore_sub p _)) TI_pcoreC sub1G.
  rewrite centsC; apply: subset_trans.
  rewrite -p_core_Fitting Fitting_pcore pcore_max ?pcore_pgroup //=.
  rewrite /normal subsetI -pcoreI pcore_sub subIset ?gFnorm //=.
  rewrite pcoreI gFsub_trans //= -/F centsC.
  case/dprodP: (nilpotent_pcoreC p nilF) => _ _ /= cFpp' _.
  rewrite centsC (subset_trans cFpp' (centS _)) //.
  have hallFp := nilpotent_pcore_Hall p nilF.
  by rewrite (sub_Hall_pcore hallFp).
have{sHp'Mp' sMp'H} eqHp'Mp': 'O_p^'(H) = 'O_p^'(M).
  apply/eqP; rewrite eqEsubset sHp'Mp'.
  apply: subset_trans (sNZqXq' p H sAH prH).
  apply: subset_trans (pcoreS _ (subsetIr _ _)).
  rewrite -setIA (setIidPr (pcore_sub _ _)) subsetI sMp'H /=.
  rewrite (mmax_normal maxM) ?gFnormal_trans //.
  by rewrite -cardG_gt1 card_pcore_nil // p_part_gt1 piZ -def_pi.
have ntHp': 'O_p^'(H) != 1.
  have [q pi_q p'q] := pi_alt p; have: D`q \subset 'O_p^'(H).
    by rewrite p_core_Fitting sub_pcore // => r; move/eqnP->.
  rewrite -proper1G; apply: proper_sub_trans; rewrite proper1G.
  by rewrite -cardG_gt1 card_pcore_nil // p_part_gt1 piD.
rewrite -(mmax_normal maxH (pcore_normal p^' H)) //= eqHp'Mp'.
by rewrite (mmax_normal maxM (pcore_normal _ _)) //= -eqHp'Mp'.
Qed.

(* This is B & G, Theorem 8.1(b). *)
Theorem SCN_Fitting_Uniqueness p M P A :
    M \in 'M -> p.-group ('F(M)) -> p.-Sylow(M) P ->
    'r_p('F(M)) >= 3 -> A \in 'SCN_3(P) ->
  [/\ p.-Sylow(G) P, A \subset 'F(M) & A \in 'U].
Proof.
set F := 'F(M) => maxM pF sylP dimFp3 scn3_A.
have [scnA dimA3] := setIdP scn3_A; have [nsAP defCA] := SCN_P scnA.
have cAA := SCN_abelian scnA; have sAP := normal_sub nsAP.
have [sPM pP _] := and3P sylP; have sAM := subset_trans sAP sPM.
have{dimA3} ntA: A :!=: 1 by case: eqP dimA3 => // ->; rewrite rank1.
have prM := mmax_proper maxM; have solM := mFT_sol prM.
have{pF} Mp'1: 'O_p^'(M) = 1.
  apply/eqP; rewrite -trivg_Fitting ?(solvableS (pcore_sub _ _)) //.
  rewrite Fitting_pcore -(setIidPr (pcore_sub _ _)) coprime_TIg //.
  exact: pnat_coprime (pcore_pgroup _ _).
have defF: F = M`p := Fitting_eq_pcore Mp'1.
have sFP: F \subset P by rewrite defF (pcore_sub_Hall sylP).
have sAF: A \subset F.
  rewrite defF -(pseries_pop2 _ Mp'1).
  exact: (odd_p_abelian_constrained (mFT_odd _) solM sylP cAA nsAP).
have sZA: 'Z(F) \subset A.
  by rewrite -defCA setISS ?centS // defF pcore_sub_Hall.
have sCAM: 'C(A) \subset M.
  have nsZM: 'Z(F) <| M by rewrite !gFnormal_trans.
  rewrite -(mmax_normal maxM nsZM); last first.
    rewrite /= -(setIidPr (center_sub _)) meet_center_nil ?Fitting_nil //.
    by rewrite -proper1G (proper_sub_trans _ sAF) ?proper1G.
  by rewrite (subset_trans _ (cent_sub _)) ?centS.
have nsZL_M: 'Z('L(P)) <| M.
  by rewrite (Puig_center_normal (mFT_odd _) solM sylP).
have sNPM: 'N(P) \subset M.
  rewrite -(mmax_normal maxM nsZL_M) ?gFnorm_trans //.
  apply/eqP => /(trivg_center_Puig_pgroup (pHall_pgroup sylP))-P1.
  by rewrite -subG1 -P1 sAP in ntA.
have sylPG: p.-Sylow(G) P := mmax_sigma_Sylow maxM sylP sNPM.
split; rewrite // (uniq_mmax_subset1 maxM sAM).
have{scn3_A} scn3_A: A \in 'SCN_3[p] by apply/bigcupP; exists P; rewrite // inE.
pose K := 'O_p^'('C(A)); have sKF: K \subset F.
  have sKM: K \subset M := gFsub_trans _ sCAM.
  apply: subset_trans (cent_sub_Fitting solM).
  rewrite subsetI sKM coprime_nil_faithful_cent_stab ?Fitting_nil //.
  - by rewrite gFsub_trans ?(subset_trans sCAM) ?gFnorm.
  - by rewrite /= -/F defF coprime_pcoreC.
  have sACK: A \subset 'C_F(K) by rewrite subsetI sAF centsC pcore_sub.
  by rewrite /= -/F -/K (subset_trans _ sACK) //= -defCA setISS ?centS.
have{sKF} K1: K = 1 by rewrite -(setIidPr sKF) defF TI_pcoreC.
have p'nbyA_1 q: q != p -> |/|*(A; q) = [set 1%G].
  move=> p'q.
  have: [transitive K, on |/|*(A; q) | 'JG] by apply: Thompson_transitivity.
  case/imsetP=> Q maxQ; rewrite K1 /orbit imset_set1 act1 => defAmax.
  have nQNA: 'N(A) \subset 'N(Q).
    apply/normsP=> x Nx; apply: congr_group; apply/set1P; rewrite -defAmax.
    by rewrite (acts_act (norm_acts_max_norm _ _)).
  have{nQNA} nQF: F \subset 'N(Q).
    exact: subset_trans (subset_trans (normal_norm nsAP) nQNA).
  have defFmax: |/|*(F; q) = [set Q] := max_normed_uniq defAmax sAF nQF.
  have nQM: M \subset 'N(Q).
    apply/normsP=> x Mx; apply: congr_group; apply/set1P; rewrite -defFmax.
    rewrite (acts_act (norm_acts_max_norm _ _)) ?defFmax ?set11 //.
    by rewrite (subsetP (gFnorm _ _)).
  have [<- // | ntQ] := eqVneq Q 1%G.
  rewrite inE in maxQ; have [qQ _] := andP (maxgroupp maxQ).
  have{nQM} defNQ: 'N(Q) = M.
    by rewrite (mmax_norm maxM) // (mFT_pgroup_proper qQ).
  case/negP: ntQ; rewrite -[_ == _]subG1 -Mp'1 -defNQ pcore_max ?normalG //.
  exact: pi_pnat qQ _.
have{p'nbyA_1} p'nbyA_1 X:
  X \proper G -> p^'.-group X -> A \subset 'N(X) -> X :=: 1.
- move=> prX p'X nXA; have solX := mFT_sol prX.
  apply/eqP; rewrite -trivg_Fitting // -subG1 /= FittingEgen gen_subG.
  apply/bigcupsP=> [[q /= _] _]; have [-> | p'q] := eqVneq q p.
    rewrite -(setIidPl (pcore_sub _ _)) coprime_TIg //.
    by rewrite (pnat_coprime (pcore_pgroup _ _)).
  have [R] := max_normed_exists (pcore_pgroup q X) (gFnorm_trans _ nXA).
  by rewrite p'nbyA_1 // => /set1P->.
apply/subsetPn=> -[H0 MA_H0 neH0M].
pose H := [arg max_(H > H0 | (H \in 'M(A)) && (H != M)) #|H :&: M|`_p].
case: arg_maxP @H => [|H {H0 MA_H0 neH0M}]; first by rewrite MA_H0 -in_set1.
rewrite /= inE -andbA => /and3P[maxH sAH neHM] maxHM.
have prH: H \proper G by rewrite inE in maxH; apply: maxgroupp maxH.
have sAHM: A \subset H :&: M by rewrite subsetI sAH.
have [R sylR_HM sAR]:= Sylow_superset sAHM (pgroupS sAP pP).
have [/subsetIP[sRH sRM] pR _] := and3P sylR_HM.
have{sylR_HM} sylR_H: p.-Sylow(H) R.
  have [Q sylQ] := Sylow_superset sRM pR; have [sQM pQ _] := and3P sylQ.
  case/eqVproper=> [defR | /(nilpotent_proper_norm (pgroup_nil pQ)) sRN].
    apply: (pHall_subl sRH (subsetT _)); rewrite pHallE subsetT /=.
    by rewrite -(card_Hall sylPG) (card_Hall sylP) defR (card_Hall sylQ).
  case/maximal_exists: (subsetT 'N(R)) => [nRG | [D maxD sND]].
    case/negP: (proper_irrefl (mem G)); rewrite -{1}nRG.
    rewrite mFT_norm_proper ?(mFT_pgroup_proper pR) //.
    by rewrite -proper1G (proper_sub_trans _ sAR) ?proper1G.
  move/implyP: (maxHM D); rewrite 2!inE {}maxD leqNgt.
  case: eqP sND => [->{D} sNM _ | _ sND].
    rewrite -Sylow_subnorm (pHall_subl _ _ sylR_HM) ?setIS //.
    by rewrite subsetI sRH normG.
  rewrite (subset_trans (subset_trans sAR (normG R)) sND); case/negP.
  rewrite -(card_Hall sylR_HM) (leq_trans (proper_card sRN)) //.
  rewrite -(part_pnat_id (pgroupS (subsetIl _ _) pQ)) dvdn_leq //.
  by rewrite partn_dvd ?cardG_gt0 // cardSg //= setIC setISS.
have Hp'1: 'O_p^'(H) = 1.
  apply: p'nbyA_1 (pcore_pgroup _ _) (subset_trans sAH (gFnorm _ _)).
  exact: sub_proper_trans (pcore_sub _ _) prH.
have nsZLR_H: 'Z('L(R)) <| H.
  exact: Puig_center_normal (mFT_odd _) (mFT_sol prH) sylR_H _.
have ntZLR: 'Z('L(R)) != 1.
  apply/eqP=> /(trivg_center_Puig_pgroup pR) R1.
  by rewrite -subG1 -R1 sAR in ntA.
have defH: 'N('Z('L(R))) = H := mmax_normal maxH nsZLR_H ntZLR.
have{sylR_H} sylR: p.-Sylow(G) R.
  rewrite -Sylow_subnorm setTI (pHall_subl _ _ sylR_H) ?normG //=.
  by rewrite -defH !gFnorm_trans.
have nsZLR_M: 'Z('L(R)) <| M.
  have sylR_M := pHall_subl sRM (subsetT _) sylR.
  exact: Puig_center_normal (mFT_odd _) solM sylR_M _.
case/eqP: neHM; apply: group_inj.
by rewrite -defH (mmax_normal maxM nsZLR_M).
Qed.

(* This summarizes the two branches of B & G, Theorem 8.1. *)
Theorem Fitting_Uniqueness M : M \in 'M -> 'r('F(M)) >= 3 -> 'F(M)%G \in 'U.
Proof.
move=> maxM; have [p _ -> dimF3] := rank_witness 'F(M).
have prF: 'F(M) \proper G := sub_mmax_proper maxM (Fitting_sub M).
have [pF | npF] := boolP (p.-group 'F(M)).
  have [P sylP] := Sylow_exists p M; have [sPM pP _] := and3P sylP.
  have dimP3: 'r_p(P) >= 3.
    rewrite (p_rank_Sylow sylP) (leq_trans dimF3) //.
    by rewrite p_rankS ?Fitting_sub.
  have [A] := rank3_SCN3 pP (mFT_odd _) dimP3.
  by case/(SCN_Fitting_Uniqueness maxM pF)=> // _ sAF; apply: uniq_mmaxS.
case/p_rank_geP: dimF3 => A /setIdP[EpA dimA3].
have [A0 maxA0 sAA0] := @maxgroup_exists _ [pred X in 'E_p('F(M))] _ EpA.
have [_ abelA] := pElemP EpA; have pmaxA0: A0 \in 'E*_p('F(M)) by rewrite inE.
case/pElemP: (maxgroupp maxA0) => sA0F; case/and3P=> _ cA0A0 _.
have dimA0_3: 'r_p(A0) >= 3.
  by rewrite -(eqP dimA3) -(p_rank_abelem abelA) p_rankS.
have:= non_pcore_Fitting_Uniqueness maxM npF pmaxA0 dimA0_3.
exact: uniq_mmaxS (subsetIl _ _) prF.
Qed.

End Eight.

author: math-comp

repo: mathcomp-history-before-github


text:
Require Export ComponentSM.

Section ComponentSM8.

  Local Open Scope eo.
  Local Open Scope proc.

  Context { pd  : @Data }.
  Context { pn  : @Node }.
  Context { pk  : @Key }.
  Context { pat : @AuthTok }.
  Context { paf : @AuthFun pn pk pat pd }.
  Context { pm  : @Msg }.
  Context { pda : @DataAuth pd pn }.
  Context { cad : ContainedAuthData }.
  Context { gms : MsgStatus }.
  Context { dtc : @DTimeContext }.
  Context { qc  : @Quorum_context pn}.
  Context { iot : @IOTrustedFun }.

  Context { base_fun_io       : baseFunIO }.
  Context { base_state_fun    : baseStateFun }.
  Context { trusted_state_fun : trustedStateFun }.

  Lemma M_run_ls_before_event_implies_has_correct_trace_before :
    forall {eo : EventOrdering} (e : Event) {L S} (ls1 ls2 : LocalSystem L S),
      ~isFirst e
      -> M_run_ls_before_event ls1 e = Some ls2
      -> has_correct_trace_before (local_pred e) (loc e).
  Proof.
    introv nf run.
    rewrite M_run_ls_before_event_unroll_on in run.
    destruct (dec_isFirst e) as [d|d]; ginv; tcsp.
    apply M_run_ls_on_event_implies_has_correct_trace_before in run; autorewrite with eo in *; auto.
  Qed.
  Hint Resolve M_run_ls_before_event_implies_has_correct_trace_before : comp.

  Lemma M_output_sys_on_event_implies_has_correct_trace_before :
    forall {eo : EventOrdering} (e : Event) {F} (sys : M_USystem F) d,
      d ∈ sys ⇝ e
      -> has_correct_trace_before e (loc e).
  Proof.
    introv out.
    apply M_output_ls_on_event_as_run in out; exrepnd.
    destruct (dec_isFirst e) as [isf|isf].

    { apply isCorrect_first_implies_has_correct_trace_before; auto.
      unfold M_output_ls_on_this_one_event in *.
      unfold isCorrect.
      remember (trigger_op e) as trig; destruct trig; tcsp. }

    apply M_run_ls_before_event_implies_has_correct_trace_before in out1; auto.
    apply has_correct_trace_before_local_pred_implies; auto.
    unfold M_output_ls_on_this_one_event in *.
    unfold isCorrect.
    remember (trigger_op e) as trig; destruct trig; tcsp.
  Qed.
  Hint Resolve M_output_sys_on_event_implies_has_correct_trace_before : comp.

End ComponentSM8.

Hint Resolve M_run_ls_before_event_implies_has_correct_trace_before : comp.
Hint Resolve M_output_sys_on_event_implies_has_correct_trace_before : comp.

author: veri-fit

repo: Asphalion

save_path: github-repos/coq/veri-fit-Asphalion


text:
(**
CoLoR, a Coq library on rewriting and termination.
See the COPYRIGHTS and LICENSE files.

- Frédéric Blanqui, 2009-03-25 (setoid), 2014-02-25 (classes)
- Adam Koprowski and Johannes Waldmann, 2008-01
*)

Set Implicit Arguments.

Require Import OrdSemiRing2 VecUtil Matrix2 AMonAlg VecArith2
  Structures.Equalities LogicUtil Morphisms RelUtil NatUtil
  AWFMInterpretation Max.

Section S.

  Context {OSR : OrderedSemiRing}.

  Import OSR_Notations.

  Record matrixInt (dim argCnt : nat) := {
    const : vector s_typ dim;
    args  : vector (matrix dim dim) argCnt }.

  Variable Sig: Signature.

  (* REMARK: make dim as a parameter *)

  Variable dim      : nat.
  Parameter dim_pos : dim > 0.

  Class TMatrixInt := {
    mi_trsInt : forall f : Sig, matrixInt dim (arity f) }.

  Class MatrixMethodConf := {
    mic_mi            :> TMatrixInt;
    mic_vec_invariant : vector s_typ dim -> Prop;
    mic_inv_id_matrix : mic_vec_invariant (id_vec dim_pos) }.

Section MatrixBasedInt.

  Context {MC : MatrixMethodConf}.

  Notation vec     := (vector s_typ dim).
  Notation eq_vec  := (Vforall2 s_eq (n:= dim)).
  Infix "=v"       := eq_vec (at level 70).
  Notation vec_ge  := (Vforall2 osr_ge (n:= dim)).
  Infix ">=v"      := vec_ge (at level 70).
  Notation mat     := (matrix dim dim).
  Notation mat_eqA := (mat_eqA dim dim).
  Notation mint    := (matrixInt dim).

  (*REMOVE?*)
  Global Instance eq_vec_eq_vec_rel k : Equivalence (Vforall2 eq_vec (n:=k)).

  Proof. class. Qed.

  Global Instance eq_vec_mat_eqA_rel k : Equivalence (Vforall2 mat_eqA (n:=k)).

  Proof. class. Qed.

  Definition eq_mint k (mi1 mi2 : mint k) :=
    let (c1, args1) := mi1 in
    let (c2, args2) := mi2 in
      c1 =v c2 /\ Vforall2 mat_eqA args1 args2.

  Notation "x =i y" := (eq_mint x y) (at level 70).

  Global Instance eq_mint_refl k : Reflexive (@eq_mint k).

  Proof. unfold eq_mint, Reflexive. destruct x. intuition. Qed.

  Global Instance eq_mint_sym k : Symmetric (@eq_mint k).

  Proof. unfold eq_mint, Symmetric. destruct x. destruct y. intuition. Qed.

  Global Instance eq_mint_trans k : Transitive (@eq_mint k).

  Proof.
    unfold eq_mint, Transitive. destruct x. destruct y. destruct z. intuition.
    trans const1; hyp. trans args1; hyp.
  Qed.

  (*REMOVE?*)
  Global Instance eq_mint_equiv k : Equivalence (@eq_mint k).

  Proof. constructor; class. Qed.

  Global Instance build_matrixInt_mor k :
    Proper (eq_vec ==> Vforall2 mat_eqA ==> @eq_mint k)
    (@Build_matrixInt dim k).

  Proof. intros v v' vv' ms ms' msms'. unfold eq_mint. intuition. Qed.

  Global Instance const_mor k :
    Proper (@eq_mint k ==> eq_vec) (@const dim k).

  Proof. destruct x. destruct y. simpl. intuition. Qed.

  Global Instance args_mor k :
    Proper (@eq_mint k ==> Vforall2 mat_eqA) (@args dim k).

  Proof. destruct x. destruct y. simpl. intuition. Qed.

  Section MBI.

    Definition dom := { v : vec | mic_vec_invariant v }.

    Definition dom2vec (d : dom) : vec := proj1_sig d.

    Definition add_matrices i m n (v : vector (matrix m n) i) :=
      Vfold_left (@mat_plus _ m n) (@zero_matrix _ m n) v.

    Definition mi_eval_aux n (mi : mint n) (v : vector vec n) : vec :=
      add_vectors (Vmap2 (@mat_vec_prod _ _ _) (args mi) v) [+] const mi.

    Global Instance mi_eval_aux_mor n :
      Proper (@eq_mint n ==> Vforall2 eq_vec ==> eq_vec) (@mi_eval_aux n).

    Proof.
      intros I I' II' v v' vv'. unfold mi_eval_aux. apply vector_plus_mor.
      apply add_vectors_mor. apply Vforall2_intro_nth. intros.
      rewrite !Vnth_map2.
      apply mat_vec_prod_mor. apply Vforall2_elim_nth. rewrite II'. refl.
      apply Vforall2_elim_nth. hyp. rewrite II'. refl.
    Qed.

    Variable mi_eval_ok : forall f v,
      mic_vec_invariant (mi_eval_aux (mi_trsInt f) (Vmap dom2vec v)).

    Definition mi_eval f (v : vector dom (arity f)) : dom :=
      exist mic_vec_invariant (mi_eval_aux (mi_trsInt f) (Vmap dom2vec v))
            (mi_eval_ok f v).

    Lemma mi_eval_cons : forall n (mi : mint (S n)) v vs,
      mi_eval_aux mi (Vcons v vs) =v
        mat_vec_prod (Vhead (args mi)) v [+]
        mi_eval_aux (Build_matrixInt (const mi) (Vtail (args mi))) vs.

    Proof.
      intros. unfold mi_eval_aux. simpl. rewrite vector_plus_assoc.
      apply vector_plus_mor. apply vector_plus_comm. refl.
    Qed.

    Definition dom_zero : dom.

    Proof. exists (id_vec dim_pos). apply mic_inv_id_matrix. Defined.

    Definition I := @mkInterpretation Sig dom dom_zero mi_eval.

    Definition succeq := Rof (Vforall2 osr_ge) dom2vec.

    Global Instance refl_succeq : Reflexive succeq.

    Proof. intro x. unfold succeq, Rof. refl. Qed.

    Global Instance trans_succeq : Transitive succeq.

    Proof. apply Rof_trans. class. Qed.

    (** Monotonicity *)

    Section VecMonotonicity.

      Variable f : matrix dim dim -> vec -> vec.
      Variable f_mon : forall M v1 v2, v1 >=v v2 -> f M v1 >=v f M v2.
      Variables (a b : vec).

      Lemma vec_add_weak_monotone_map2 : forall n1 (v1 : vector vec n1) n2
        (v2 : vector vec n2) n (M : vector (matrix dim dim) n) i_j, a >=v b ->
        add_vectors (Vmap2 f M (Vcast (Vapp v1 (Vcons a v2)) i_j)) >=v
        add_vectors (Vmap2 f M (Vcast (Vapp v1 (Vcons b v2)) i_j)).

      Proof.
        induction v1; intros; simpl.
        destruct n; try solve [absurd_arith].
        unfold add_vectors, succeq. simpl. apply Vforall2_intro_nth.
        intros. unfold vector_plus. do 2 rewrite Vnth_map2.
        assert (Vnth (f (Vhead M) a) ip >>= Vnth (f (Vhead M) b) ip).
        apply Vforall2_elim_nth. apply f_mon. hyp.
        apply osr_add_ge. apply osr_ge_refl. hyp.
        destruct n0; try solve [absurd_arith].
        unfold add_vectors, succeq. simpl. apply Vforall2_intro_nth.
        intros. unfold vector_plus. do 2 rewrite Vnth_map2.
        apply osr_add_ge.
        apply Vforall2_elim_nth. unfold add_vectors in IHv1. apply IHv1.
        hyp. apply osr_ge_refl.
      Qed.

    End VecMonotonicity.

    Lemma monotone_succeq : monotone I succeq.

    Proof.
      intros f i j i_j vi vj a b ab.
      simpl. unfold mi_eval, mi_eval_aux, succeq. simpl.
      apply vec_plus_ge_compat_r.
      do 2 rewrite Vmap_cast. do 2 rewrite Vmap_app. simpl.
      apply vec_add_weak_monotone_map2; trivial.
      intros. unfold succeq. apply Vforall2_intro_nth. intros.
      unfold mat_vec_prod. do 2 rewrite Vnth_col_mat. apply mat_mult_mon.
      apply mat_ge_refl. intros x y xp yp.
      do 2 rewrite vec_to_col_mat_spec.
      apply Vforall2_elim_nth. hyp.
    Qed.

    Lemma succeq_dec : rel_dec succeq.

    Proof.
      intros x y. unfold succeq. apply Vforall2_dec.
      intros m n. apply osr_ge_dec.
    Defined.

    (** decidability of order on terms induced by matrix interpretations *)

    Section OrderDecidability.

      Require Import ABterm.

      Notation bterm := (bterm Sig).

      (** symbolic computation of term interpretation *)

      Definition mat_matrixInt_prod n M (mi : mint n) : mint n :=
        Build_matrixInt (mat_vec_prod M (const mi))
                    (Vmap (mat_mult M) (args mi)).

      Definition combine_matrices n k (v : vector (vector mat k) n) :=
        Vbuild (fun i ip => add_matrices (Vmap (fun v => Vnth v ip) v)).

      Lemma combine_matrices_nil : forall i,
        combine_matrices Vnil = Vconst (@zero_matrix _ dim dim) i.

      Proof.
        intros. apply Veq_nth. intros. unfold combine_matrices.
        rewrite Vnth_const. rewrite Vbuild_nth. trivial.
      Qed.

      Lemma combine_matrices_cons :
        forall k n v (vs : vector (vector mat k) n),
          combine_matrices (Vcons v vs) =
          Vmap2 (@mat_plus _ _ _) (combine_matrices vs) v.

      Proof.
        intros. apply Veq_nth. intros.
        unfold combine_matrices, add_matrices. simpl.
        rewrite Vnth_map2. do 2 rewrite Vbuild_nth. refl.
      Qed.

      Fixpoint mi_of_term k (t : bterm k) : mint (S k) :=
        match t with
          | BVar i ip =>
            let zero_int := Vconst (@zero_matrix _ dim dim) (S k) in
            let args_int := Vreplace zero_int (le_lt_S ip) (@id_matrix _ dim) in
            Build_matrixInt (@zero_vec _ dim) args_int
          | BFun f v =>
            let f_int := mi_trsInt f in
            let args_int := Vmap (@mi_of_term k) v in
            let args_int' := Vmap2 (@mat_matrixInt_prod (S k))
                                   (args f_int) args_int in
            let res_const := add_vectors (Vcons (const f_int)
              (Vmap (@const dim (S k)) args_int')) in
            let res_args := combine_matrices (Vmap (@args _ _) args_int') in
            Build_matrixInt res_const res_args
        end.

      Require Import ATrs.

      Definition rule_mi r :=
        let mvl := maxvar (lhs r) in
        let mvr := maxvar (rhs r) in
        let m := max mvl mvr in
        let lt := inject_term (le_max_l mvl mvr) in
        let rt := inject_term (le_max_r mvl mvr) in
          (mi_of_term lt, mi_of_term rt).

      (** order characteristic for symbolically computed interpretation and
       its decidability *)

      Notation mat_ge := (@mat_ge _ dim dim).

      Definition mint_ge n (l r : mint n) :=
        Vforall2 mat_ge (args l) (args r)
        /\ Vforall2 osr_ge (const l) (const r).

      (* Add: Boolean function of [mint_ge]. *)

      Require Import BoolUtil.

      Definition bmint_ge n (l r : mint n) : bool :=
        bVforall2 (bmat_ge (n:=dim))(args l) (args r) &&
                  bVforall2 (fun m n => bge _ m n) (const l) (const r).

      (** Add: Correctness proof of [mint_ge] over domain natural numbers. *)

      Lemma bmint_ge_ok : forall n (l r: mint n),
                            bmint_ge l r = true <-> mint_ge l r.

      Proof.
        intros n l r. intuition.
        (* [1]. Proving the <- *)
        unfold bmint_ge in H. rewrite andb_eq in H. destruct H.
        unfold mint_ge. split.
        (* Left part. *)
        rewrite bVforall2_ok in H. apply H.
        (* Proving boolean function of [bmat_ge]. *)
        intros M N. split.
        (* -> *)
        intro H1. apply bmat_ge_ok. hyp.
        (* <- *)
        intro H1. rewrite bmat_ge_ok. hyp.
        (* Right part. *)
        rewrite bVforall2_ok in H0. apply H0.
        (* Proving boolean function of [bge]. *)
        intros x y. split.
        (* -> *)
        intro H1. apply bge_ok. hyp.
        (* <- *)
        intro H1. rewrite bge_ok. hyp.
        (* [2]. Proving the -> *)
        unfold bmint_ge. rewrite andb_eq. split.
        (* Left part. *)
        rewrite bVforall2_ok. unfold mint_ge in H.
        destruct H. apply H.
        (* Proving boolean function of [bmat_ge]. *)
        intros M N. split.
        (* -> *)
        intro H1. apply bmat_ge_ok. hyp.
        (* <- *)
        intro H1. rewrite bmat_ge_ok. hyp.
        (* Right part. *)
        rewrite bVforall2_ok. unfold mint_ge in H.
        destruct H. apply H0.
        (* Proving boolean function of [bge]. *)
        intros x y. split.
        (* -> *)
        intro H1. apply bge_ok. hyp.
        (* <- *)
        intro H1. rewrite bge_ok. hyp.
      Qed.

      Definition term_ord (ord : forall n, relation (mint n)) l r :=
        let (li, ri) := rule_mi (mkRule l r) in ord _ li ri.

      Variable mint_gt : forall n (l r : mint n), Prop.
      Variable mint_gt_dec : forall n, rel_dec (@mint_gt n).

      Definition term_ge := term_ord mint_ge.
      Definition term_gt := term_ord mint_gt.

      Lemma mint_ge_dec : forall n, rel_dec (@mint_ge n).

      Proof.
        intros n x y. unfold mint_ge.
        destruct (Vforall2_dec (@mat_ge_dec _ _ _) (args x) (args y));
          intuition.
        destruct (Vforall2_dec osr_ge_dec (const x) (const y)); intuition.
      Defined.

      Lemma term_ge_dec : rel_dec term_ge.

      Proof.
        intros l r. unfold term_ge, term_ord. simpl.
        match goal with |- {mint_ge ?l ?r} + {~mint_ge ?l ?r} =>
                        destruct (mint_ge_dec l r); auto
        end.
      Defined.

      Lemma term_gt_dec : rel_dec term_gt.

      Proof.
        intros l r. unfold term_gt, term_ord. simpl.
        match goal with |- {mint_gt ?l ?r} + {~mint_gt ?l ?r} =>
                        destruct (mint_gt_dec l r); auto
        end.
      Defined.

      Notation IR_succeq := (IR I succeq).

      Definition mint_eval (val : valuation I) k (mi : mint k) : vec :=
        let coefs := Vbuild (fun i (ip : i < k) => dom2vec (val i)) in
        add_vectors (Vcons (const mi) (Vmap2 (@mat_vec_prod _ _ _) (args mi) coefs)).

      Global Instance mint_eval_mor k val :
        Proper (@eq_mint k ==> eq_vec) (@mint_eval val k).

      Proof.
        intros [c1 args1] [c2 args2]. unfold eq_mint. intuition.
        unfold mint_eval. simpl. apply add_vectors_mor.
        rewrite Vforall2_cons_eq. intuition.
        apply Vmap2_proper with (R := mat_eqA) (S := eq_vec).
        apply mat_vec_prod_mor. hyp. refl.
      Qed.

      Lemma mint_eval_split : forall val k (mi : mint k),
        let coefs := Vbuild (fun i (ip : i < k) => dom2vec (val i)) in
          mint_eval val mi =v const mi [+]
          add_vectors (Vmap2 (@mat_vec_prod _ _ _) (args mi) coefs).

      Proof.
        intros. unfold mint_eval, add_vectors. simpl.
        rewrite vector_plus_comm. refl.
      Qed.

      Lemma mint_eval_var_aux : forall M i k (v : vector vec k) (ip : i < k),
        add_vectors (Vmap2 (@mat_vec_prod _ _ _) (Vreplace (Vconst
          (@zero_matrix _ dim dim) k) ip M) v) =v
          col_mat_to_vec (M <*> (vec_to_col_mat (Vnth v ip))).

      Proof.
        induction i; intros.
        destruct k. absurd_arith.
        unfold add_vectors. simpl.
        fold (add_vectors (Vmap2 (@mat_vec_prod _ _ _)
                                 (Vconst (@zero_matrix _ dim dim) k) (Vtail v))).
        assert (add_vectors
          (Vmap2 (@mat_vec_prod _ _ _) (Vconst (@zero_matrix _ dim dim) k) (Vtail v))
          =v @zero_vec _ dim). Focus 2. rewrite H.
        rewrite vector_plus_zero_l.
        replace (Vhead v) with (Vnth v ip). refl.
        rewrite Vhead_nth. rewrite (lt_unique (lt_O_Sn k) ip). refl.
        apply add_vectors_zero. apply Vforall_nth_intro. intros.
        rewrite Vnth_map2. rewrite Vnth_const.
        unfold mat_vec_prod. rewrite zero_matrix_mult_l.
        apply Vforall2_intro_nth. intros. rewrite Vnth_col_mat.
        unfold zero_matrix, zero_vec.
        rewrite mat_build_elem. rewrite Vnth_const. refl.
        destruct k. absurd_arith.
        rewrite Vreplace_tail. simpl. rewrite add_vectors_cons.
        unfold mat_vec_prod at 1. rewrite zero_matrix_mult_l.
        assert (col_mat_to_vec (@zero_matrix _ dim 1) =v @zero_vec _ dim).
        apply Vforall2_intro_nth. intros. rewrite Vnth_col_mat.
        unfold zero_matrix, zero_vec.
        rewrite mat_build_elem. rewrite Vnth_const. refl. rewrite H.
        rewrite vector_plus_zero_l. rewrite IHi. rewrite Vnth_tail.
        rewrite (le_unique (lt_n_S (lt_S_n ip)) ip). refl.
      Qed.

      Lemma mint_eval_eq_term_int_var : forall v (val : valuation I) k
                                               (t_b : maxvar_le k (Var v)),
        dom2vec (bterm_int val (inject_term t_b)) =v
        mint_eval val (mi_of_term (inject_term t_b)).

      Proof.
        intros. rewrite mint_eval_split.
        change (const (mi_of_term (inject_term t_b))) with (@zero_vec _ dim).
        rewrite vector_plus_zero_l.
        change (args (mi_of_term (inject_term t_b))) with (Vreplace (Vconst
          (@zero_matrix _ dim dim) (S k)) (le_lt_S (maxvar_var t_b))
          (@id_matrix _ dim)).
        rewrite mint_eval_var_aux. rewrite Vbuild_nth. simpl.
        trans (col_mat_to_vec (vec_to_col_mat (dom2vec (val v)))).
        rewrite col_mat_to_vec_idem. refl. apply get_col_mor.
        rewrite mat_mult_id_l. refl. ded dim_pos. auto.
      Qed.

      Lemma mint_eval_const : forall val k (c : vec),
        mint_eval (k:=k) val (Build_matrixInt c (combine_matrices Vnil)) =v c.

      Proof.
        intros. unfold mint_eval. simpl. autorewrite with arith.
        trans (c [+] @zero_vec _ dim). apply vector_plus_mor. refl.
        apply add_vectors_zero. apply Vforall_nth_intro. intros.
        rewrite Vnth_map2. rewrite combine_matrices_nil. rewrite Vnth_const.
        unfold mat_vec_prod. apply Vforall2_intro_nth. intros.
        rewrite Vnth_col_mat.
        trans (get_elem (@zero_matrix _ dim 1) ip0 access_0).
        apply get_elem_mor. apply zero_matrix_mult_l.
        unfold zero_matrix. rewrite mat_build_elem.
        unfold zero_vec. rewrite Vnth_const. refl.
        apply vector_plus_zero_r.
      Qed.

      Lemma mint_eval_cons : forall n k val c_hd c_tl a_hd
                                    (a_tl : vector (vector mat k) n),
        mint_eval val (Build_matrixInt (c_hd [+] c_tl)
          (combine_matrices (Vcons a_hd a_tl))) =v
        mint_eval val (Build_matrixInt c_hd a_hd) [+]
        mint_eval val (Build_matrixInt c_tl (combine_matrices a_tl)).

      Proof.
        intros. unfold mint_eval. simpl.
        set (vali := Vbuild (A := vec) (fun i (_ : i < k) => dom2vec (val i))).
        rewrite combine_matrices_cons.
        autorewrite with arith. rewrite <- !vector_plus_assoc.
        apply vector_plus_mor. refl. rewrite vector_plus_assoc.
        rewrite (vector_plus_comm _ c_tl). rewrite <- vector_plus_assoc.
        apply vector_plus_mor. refl. apply add_vectors_split. intros.
        rewrite !Vnth_map2, vector_plus_comm. apply mat_vec_prod_distr_mat.
      Qed.

      Lemma mint_eval_mult_factor : forall k val M (mi : mint k),
        mint_eval val (mat_matrixInt_prod M mi) =v
        mat_vec_prod M (mint_eval val mi).

      Proof.
        unfold mint_eval. intros. simpl. autorewrite with arith.
        rewrite mat_vec_prod_distr_vec. apply vector_plus_mor. refl.
        set (gen := Vbuild (A:=vec) (fun i (_ : i < k) => dom2vec (val i))).
        rewrite (mat_vec_prod_distr_add_vectors M
          (Vmap2 (@mat_vec_prod _ _ _) (args mi) gen)
          (Vmap2 (@mat_vec_prod _ _ _) (Vmap (mat_mult M) (args mi)) gen)).
        refl. intros. rewrite !Vnth_map2, Vnth_map.
        unfold mat_vec_prod. rewrite vec_to_col_mat_idem.
        apply get_col_mor. rewrite mat_mult_assoc. refl.
      Qed.

      Lemma mint_eval_eq_bterm_int_fapp : forall k i fi val
                                                 (v : vector (bterm k) i),
        let arg_eval := Vmap2 (@mat_matrixInt_prod (S k)) (args fi)
          (Vmap (@mi_of_term k) v) in
          mi_eval_aux fi (Vmap
            (fun t : bterm k => mint_eval val (mi_of_term t)) v) =v
          mint_eval val (Build_matrixInt
            (add_vectors (Vcons (const fi) (Vmap
              (@const dim (S k)) arg_eval)))
            (combine_matrices (Vmap (@args dim (S k)) arg_eval))).

      Proof.
        induction i; intros.
        (* i = 0 *)
        VOtac. simpl.
        unfold mi_eval_aux, add_vectors. simpl. autorewrite with arith.
        sym. apply mint_eval_const.
        (* i > 0 *)
        VSntac v. simpl mi_eval_aux.
        rewrite mi_eval_cons. rewrite IHi. simpl.
        (* FIXME: morphisms do work here ? *)
        trans (@mint_eval val (S k)
          (@Build_matrixInt dim (S k)
            (@mat_vec_prod _ dim dim
                       (@Vhead (matrix dim dim) i
                          (@args dim (S i) fi))
                       (@const dim (S k)
                          (@Vhead (mint (S k)) i
                             (@Vmap (ABterm.bterm Sig k)
                                (mint (S k))
                                (@mi_of_term k) (S i) v)))
                 [+] @add_vectors _ dim (S i) (@Vcons (vector _ dim)
                     (@const dim (S i) fi) i
                    (@Vmap (mint (S k))
                       (vector _ dim) (@const dim (S k)) i
                       (@Vmap2 (matrix dim dim)
                          (mint (S k))
                          (mint (S k))
                          (@mat_matrixInt_prod (S k)) i
                          (@Vtail (matrix dim dim) i
                             (@args dim (S i) fi))
                          (@Vtail (mint (S k)) i
                             (@Vmap (ABterm.bterm Sig k)
                                (mint (S k))
                                (@mi_of_term k) (S i) v))))))
           (@combine_matrices (S i) (S k)
              (@Vcons (vector (matrix dim dim) (S k))
                 (@Vmap (matrix dim dim) (matrix dim dim)
                    (@mat_mult _ dim dim dim
                       (@Vhead (matrix dim dim) i
                          (@args dim (S i) fi)))
                    (S k)
                    (@args dim (S k)
                       (@Vhead (mint (S k)) i
                          (@Vmap (ABterm.bterm Sig k)
                             (mint (S k))
                             (@mi_of_term k) (S i) v)))) i
                 (@Vmap (mint (S k))
                    (vector (matrix dim dim) (S k))
                    (@args dim (S k)) i
                    (@Vmap2 (matrix dim dim)
                       (mint (S k))
                       (mint (S k))
                       (@mat_matrixInt_prod (S k)) i
                       (@Vtail (matrix dim dim) i
                          (@args dim (S i) fi))
                       (@Vtail (mint (S k)) i
                          (@Vmap (ABterm.bterm Sig k)
                             (mint (S k))
                             (@mi_of_term k) (S i) v)))))))).
        Focus 2. apply mint_eval_mor. split. rewrite add_vectors_perm.
        rewrite (add_vectors_cons (i := S i) (mat_vec_prod (Vhead (args fi))
          (const (Vhead (Vmap (mi_of_term (k:=k)) v))))). refl.
        refl.
        rewrite mint_eval_cons. apply vector_plus_mor.
        Focus 2. rewrite Vmap_tail. refl.
        rewrite H. simpl.
        fold (mat_matrixInt_prod (Vhead (args fi)) (mi_of_term (Vhead v))).
        sym. apply mint_eval_mult_factor.
      Qed.

      Lemma mint_eval_eq_bterm_int : forall (val : valuation I) t k
                                            (t_b : maxvar_le k t),
        dom2vec (bterm_int val (inject_term t_b)) =v
        mint_eval val (mi_of_term (inject_term t_b)).

      Proof.
        intros val t. pattern t. apply term_ind_forall; intros.
        apply mint_eval_eq_term_int_var.
        rewrite inject_term_eq. simpl.
        rewrite Vmap_map.
        rewrite (@Vforall2_map_intro _ _ eq_vec
          (fun x => dom2vec (bterm_int val x))
          (fun (t : bterm k) => mint_eval val (mi_of_term t))).
        apply mint_eval_eq_bterm_int_fapp.
        apply Vforall_nth_intro. intros.
        rewrite inject_terms_nth. apply (Vforall_nth ip H).
      Qed.

      Lemma mint_eval_eq_term_int : forall t (val : valuation I) k
        (t_b : maxvar_le k t),
        dom2vec (term_int val t) =v
        mint_eval val (mi_of_term (inject_term t_b)).

      Proof.
        intros. rewrite <- (term_int_eq_bterm_int val t_b).
        apply mint_eval_eq_bterm_int.
      Qed.

      Lemma mint_eval_equiv : forall l r (val : valuation I),
        let (li, ri) := rule_mi (mkRule l r) in
        let lev := term_int val l in
        let rev := term_int val r in
        let lv := mint_eval val li in
        let rv := mint_eval val ri in
          lv =v dom2vec lev /\ rv =v dom2vec rev.

      Proof.
        intros. simpl. split.
        rewrite (mint_eval_eq_term_int val (le_max_l (maxvar l) (maxvar r))).
        refl.
        rewrite (mint_eval_eq_term_int val (le_max_r (maxvar l) (maxvar r))).
        refl.
      Qed.

      Lemma mint_eval_mon_succeq_args : forall k (val : vector vec k)
        (mi mi' : mint k), mint_ge mi mi' ->
        add_vectors (Vmap2 (@mat_vec_prod _ _ _) (args mi) val) >=v
        add_vectors (Vmap2 (@mat_vec_prod _ _ _) (args mi') val).

      Proof.
        destruct mi. gen val. clear val. induction args0. intros.
        destruct mi'. VOtac.
        unfold mint_eval, add_vectors. simpl. refl.
        intros. destruct mi'. VSntac args1.
        unfold mint_eval, add_vectors. simpl.
        destruct H. apply (@vec_plus_ge_compat _ dim).
        apply (IHargs0 (Vtail val) (Build_matrixInt const1 (Vtail (args1)))).
        split. simpl. change args0 with (Vtail (Vcons h args0)).
        apply Vforall2_tail. hyp. hyp.
        apply mat_vec_prod_ge_compat.
        change h with (Vhead (Vcons h args0)). do 2 rewrite Vhead_nth.
        apply Vforall2_elim_nth. hyp. refl.
      Qed.

      Lemma mint_eval_mon_succeq : forall (val : valuation I) k
        (mi mi' : mint k), mint_ge mi mi' ->
        mint_eval val mi >=v mint_eval val mi'.

      Proof.
        intros. unfold mint_eval, add_vectors. simpl.
        apply (@vec_plus_ge_compat _ dim).
        exact (mint_eval_mon_succeq_args _ H).
        destruct H. hyp.
      Qed.

      Lemma term_ge_incl_succeq : term_ge << IR_succeq.

      Proof.
        intros l r lr v. destruct (mint_eval_equiv l r v). simpl in * .
        unfold succeq, Rof. rewrite <- (vec_ge_mor H H0).
        apply mint_eval_mon_succeq. hyp.
      Qed.

      Definition succeq' := term_ge.
      Definition succeq'_sub := term_ge_incl_succeq.
      Definition succeq'_dec := term_ge_dec.

      (* FIXME: define MonotoneAlgebra for matrix *)

      (* REMARK: does not has succ *)

    End OrderDecidability.

  End MBI.

End MatrixBasedInt.

End S.

author: fblanqui

repo: rainbow

save_path: github-repos/coq/fblanqui-rainbow