text:
(**
  Ciro Iván García López
  Tesis de Maestría
  Session Type Systems Verification
  Unam - 2021

  This file contains the basic facts concerning names.
*)
From Coq Require Import Ensembles.
From Coq Require Import Finite_sets.
From Coq Require Import Finite_sets_facts.
From Coq Require Import Bool.Bool.
From Coq Require Import Arith.PeanoNat.
From Coq Require Import Arith.EqNat.
From Coq Require Import Lia.

From Tmcod Require Import Defs_Tactics.
From Tmcod Require Import Defs_Process.
From Tmcod Require Import Facts_Names.

(**
*)
Lemma There_Is_A_Name :
forall ( P : Process ),
exists ( x : nat ), ~ ( x ∈ (FVars P) ).
Proof.
Admitted.
#[global]
Hint Resolve There_Is_A_Name : Piull.

(**
*)
Lemma FVar_Process_Is_Or_Not :
forall (P : Process)( x : nat),
(x ∈ FVars P) \/ (~ x ∈ FVars P).
Admitted.
#[global]
Hint Resolve FVar_Process_Is_Or_Not : Piull.

(**
*)
Lemma No_Union_No_Each :
forall (x : nat)( X Y : FVarsE ),
~(x ∈ (X ∪ Y)) -> ~(x ∈ X) /\ ~(x ∈ Y).
Proof.
  unfold not in *.
  intros.
  constructor;
   intros;
   apply H; OrSearch.
Qed.
#[global]
Hint Resolve No_Union_No_Each : Piull.

(**
*)
Lemma FVars_Name_Finite :
forall (x : Name),
Finite _ (FVars_Name x).
Proof.
  destruct x.
  + simpl. apply Singleton_is_finite.
  + simpl. constructor.
Qed.
#[global]
Hint Resolve FVars_Name_Finite : Piull.

(**
*)
Lemma FVars_Finite :
forall (P : Process),
Finite _ (FVars P).
Proof.
  induction P;
  repeat apply Union_preserves_Finite;
  repeat apply FVars_Name_Finite;
  Piauto.
  constructor.
Qed.
#[global]
Hint Resolve FVars_Finite : Piull.

(**
*)
Lemma FVars_Name_No_Close :
forall (z k : nat)(x : Name),
~ (z ∈ FVars_Name x) -> (Close_Name k z x = x).
Proof.
  unfold not.
  intros.
  destruct x; Piauto.
  simpl.
  DecidSimple x z.
  apply beq_nat_true in e.
  rewrite e in H.
  assert ( HB : z ∈ Singleton nat z); try constructor.
  contradiction.
Qed.
#[global]
Hint Resolve FVars_Name_No_Close : Piull.

(**
*)
Lemma FVars_Bex_Name :
forall ( x : Name)(i j : nat),
FVars_Name (Bex_Name i j x) = FVars_Name x.
Proof.
  destruct x; Piauto.
  intros; simpl.
  DecidSimple i i0.
  rewrite n.
  DecidSimple i j.
Qed.
#[global]
Hint Resolve FVars_Bex_Name : Piull.

(**
*)
Lemma FVars_Bex_Process:
forall (P : Process)(i j : nat),
FVars P = FVars ({i <~> j} P).
Proof.
  InductionProcessRev P FVars_Bex_Name.
Qed.
#[global]
Hint Resolve FVars_Bex_Process : Piull.

(**
*)
Lemma Close_NoFVar_Eq :
forall ( P : Process )(z k: nat),
~ ( z ∈ (FVars P) ) -> ( Close_Rec k z P ) = P.
Proof.
  induction P; intros;
    try simpl in *;
    repeat (apply No_Union_No_Each in H; destruct H as [H ?HA]);
    repeat (rewrite IHP || rewrite IHP1 || rewrite IHP2);
    repeat rewrite FVars_Name_No_Close;
    Piauto.
Qed.
#[global]
Hint Resolve Close_NoFVar_Eq : Piull.

(**
*)
Lemma Cong_FVars :
forall (P Q : Process),
P === Q -> FVars P = FVars Q.
Proof.
  intros.
  induction H.
  + simpl.
    apply Extensionality_Ensembles.
    constructor.
    - unfold Included.
      intros.
      apply Union_inv in H.
      destruct H.
      * apply Union_inv in H.
        destruct H.
        ++ OrSearch.
        ++ OrSearch.
      * OrSearch.
    - unfold Included.
      intros.
      apply Union_inv in H.
      destruct H.
      * OrSearch.
      * apply Union_inv in H.
        destruct H.
        ++ OrSearch.
        ++ OrSearch.
  + simpl.
    apply Extensionality_Ensembles.
    constructor.
    - unfold Included.
      intros.
      apply Union_inv in H0.
      destruct H0.
      * OrSearch.
      * OrSearch.
    - unfold Included.
      intros.
      apply Union_inv in H0.
      destruct H0.
      * OrSearch.
      * OrSearch.
Qed.
#[global]
Hint Resolve Cong_FVars : Piull.
(**
Proof.
  intros.
  induction H; simpl; Piauto;
  try apply Extensionality_Ensembles;
  try constructor;
  try unfold Included;
  try intros;
  repeat (apply Union_inv in H; destruct H);
  try OrSearch.
Qed.
#[global]
Hint Resolve Cong_FVars : Piull.
*)

(**
*)
Lemma No_FVars_Parallel :
forall (P Q : Process)( u : nat),
( ~(u ∈ FVars (P ↓ Q))) -> (~ u ∈ FVars P) /\ (~ u ∈ FVars Q).
Proof.
  unfold not.
  intros.
  constructor;
  (intros; assert ( HA : u ∈ FVars (P ↓ Q)); OrSearch).
Qed.
#[global]
Hint Resolve No_FVars_Parallel : Piull.

(**
*)
Lemma In_FVars_Name_Subst :
forall (u x x1 : nat),
u ∈ FVars_Name (Subst_Name u x (FName x1)) ->
x = x1 \/ u <> u.
Proof.
  intros.
  simpl in H.
  destruct (bool_dec (x1 =? u) true).
  * rewrite e in H.
    simpl in H.
    apply Singleton_inv in H.
    apply beq_nat_true in e.
    rewrite e.
    OrSearch.
  * apply not_true_iff_false in n.
    rewrite n in H.
    simpl in H.
    apply Singleton_inv in H.
    rewrite H in n.
    apply beq_nat_false in n.
    contradiction.
Qed.
#[global]
Hint Resolve In_FVars_Name_Subst : Piull.

Require Import Coq.Program.Equality.

(**
*)
Lemma After_Subst_No_FVar :
forall (P : Process)(u x : nat),
u <> x ->
~ (u ∈ FVars ({x \ u} P)).
Proof.
  unfold not.
  intro.
  dependent induction P;
  intros; try simpl in H0;
  try apply Union_inv in H0.
  + inversions H0.
  + destruct H0.
    - apply (Subst_Name_Gen_Output u x0 x); auto.
    - apply (Subst_Name_Gen_Output u x0 y); auto.
  + destruct H0.
    - apply (IHP1 u x); auto.
    - apply (IHP2 u x); auto.
  + destruct H0.
    apply Union_inv in H0.
    destruct H0.
    - apply (Subst_Name_Gen_Output u x0 x); auto.
    - apply (Subst_Name_Gen_Output u x0 y); auto.
    - apply (IHP u x0); auto.
  + apply (Subst_Name_Gen_Output u x0 x); auto.
  + destruct H0.
    - apply (Subst_Name_Gen_Output u x0 x); auto.
    - apply (IHP u x0); auto.
  + apply (IHP u x); auto.
  + destruct H0.
    - apply (Subst_Name_Gen_Output u x0 x); auto.
    - apply (IHP u x0); auto.
  + destruct H0.
    - apply (Subst_Name_Gen_Output u x0 x); auto.
    - apply (IHP u x0); auto.
Qed.
#[global]
Hint Resolve After_Subst_No_FVar : Piull.

(**
*)
Lemma FVars_Close_Beq_Names :
forall(x : Name)(u x0 i : nat),
u <> x0 -> u ∈ FVars_Name x ->
Close_Name i x0 x = FName u.
Proof.
  intros.
  destruct x; simpl in H0; try contradiction; auto.
  apply Singleton_inv in H0.
  simpl.
  DecidSimple x x0.
Qed.
#[global]
Hint Resolve FVars_Close_Beq_Names : Piull.

(**
*)
Lemma FVars_Close_Beq :
forall ( P : Process ) (u x i : nat),
u <> x -> u ∈ FVars P -> u ∈ FVars (Close_Rec i x P).
Proof.
  induction P; intros;
  try simpl in H0; try apply Union_inv in H0; Piauto.
  + destruct H0.
    - OrSearchRew (FVars_Close_Beq_Names x u x0 i).
    - OrSearchRew (FVars_Close_Beq_Names y u x0 i).
  + destruct H0.
    - OrSearchApp (IHP1).
    - OrSearchApp (IHP2).
  + destruct H0.
    - apply Union_inv in H0.
      destruct H0.
      * OrSearchRew (FVars_Close_Beq_Names x u x0 i).
      * OrSearchRew (FVars_Close_Beq_Names y u x0 i).
    - OrSearchApp (IHP).
  + simpl.
    OrSearchRew (FVars_Close_Beq_Names x u x0 i).
  + destruct H0.
    - OrSearchRew (FVars_Close_Beq_Names x u x0 i).
    - OrSearchApp (IHP).
  + simpl; apply IHP; auto.
  + destruct H0.
    - OrSearchRew (FVars_Close_Beq_Names x u x0 i).
    - OrSearchApp (IHP).
  + destruct H0.
    - OrSearchRew (FVars_Close_Beq_Names x u x0 i).
    - OrSearchApp (IHP).
Qed.
#[global]
Hint Resolve FVars_Close_Beq : Piull.

(**
*)
Lemma FVars_Open_Beq_Names :
forall (x : Name)(u x0 i: nat),
u ∈ FVars_Name x -> FVars_Name (Open_Name i x0 x) = Singleton nat u.
Proof.
  intros.
  destruct x; simpl in H; try contradiction.
  apply Singleton_inv in H.
  rewrite H.
  auto.
Qed.
#[global]
Hint Resolve FVars_Open_Beq_Names : Piull.

(**
*)
Lemma FVars_Open_Beq_Names_Inv :
forall (x : Name)(u x0 i: nat),
u <> x0 -> u ∈ FVars_Name (Open_Name i x0 x) ->
FVars_Name x = Singleton nat u.
Proof.
  intros.
  destruct x.
  + simpl in H0.
    apply Singleton_inv in H0.
    simpl.
    auto.
  + simpl in H0.
    destruct (bool_dec (i =? i0) true).
    - rewrite e in H0.
      simpl in H0.
      apply Singleton_inv in H0.
      rewrite H0 in H.
      contradiction.
    - apply not_true_iff_false in n.
      rewrite n in H0.
      simpl in H0.
      contradiction.
Qed.
#[global]
Hint Resolve FVars_Open_Beq_Names_Inv : Piull.

(**
*)
Lemma FVars_Open_Beq :
forall ( P : Process)(u x i: nat),
u <> x -> ( u ∈ FVars P <-> u ∈ FVars ({i ~> x}P)).
Proof.
  intro.
  induction P; intros; simpl; try constructor; try intros; try contradiction.
  + apply Union_inv in H0.
    destruct H0.
    - OrSearchRew (FVars_Open_Beq_Names x u x0 i).
    - OrSearchRew (FVars_Open_Beq_Names y u x0 i).
  + apply Union_inv in H0.
    destruct H0.
    - OrSearchRew (FVars_Open_Beq_Names_Inv x u x0 i).
    - OrSearchRew (FVars_Open_Beq_Names_Inv y u x0 i).
  + apply Union_inv in H0.
    destruct H0.
    - OrSearchApp (IHP1).
    - OrSearchApp (IHP2).
  + apply Union_inv in H0.
    destruct H0.
    - left.
      apply <- (IHP1 u x i); auto.
    - right.
      apply <- (IHP2 u x i); auto.
  + apply Union_inv in H0.
    destruct H0.
    - apply Union_inv in H0.
      destruct H0.
      * OrSearchRew (FVars_Open_Beq_Names x u x0 i).
      * OrSearchRew (FVars_Open_Beq_Names y u x0 i).
    - OrSearchApp (IHP).
  + apply Union_inv in H0.
    destruct H0.
    - apply Union_inv in H0.
      destruct H0.
      * OrSearchRew (FVars_Open_Beq_Names_Inv x u x0 i).
      * OrSearchRew (FVars_Open_Beq_Names_Inv y u x0 i).
    - right.
      apply <- (IHP u x0 i); auto.
  + OrSearchRew (FVars_Open_Beq_Names x u x0 i).
  + OrSearchRew (FVars_Open_Beq_Names_Inv x u x0 i).
  + apply Union_inv in H0.
    destruct H0.
    - OrSearchRew (FVars_Open_Beq_Names x u x0 i).
    - OrSearchApp (IHP).
  + apply Union_inv in H0.
    destruct H0.
    - OrSearchRew (FVars_Open_Beq_Names_Inv x u x0 i).
    - right; apply <- (IHP u x0 i); auto.
  + apply IHP; auto.
  + apply <- (IHP u x (S i)); auto.
  + apply Union_inv in H0.
    destruct H0.
    - OrSearchRew (FVars_Open_Beq_Names x u x0 i).
    - OrSearchApp (IHP).
  + apply Union_inv in H0.
    destruct H0.
    - OrSearchRew (FVars_Open_Beq_Names_Inv x u x0 i).
    - right; apply <- (IHP u x0 (S i)); auto.
  + apply Union_inv in H0.
    destruct H0.
    - OrSearchRew (FVars_Open_Beq_Names x u x0 i).
    - OrSearchApp (IHP).
  + apply Union_inv in H0.
    destruct H0.
    - OrSearchRew (FVars_Open_Beq_Names_Inv x u x0 i).
    - right; apply <- (IHP u x0 (S i)); auto.
Qed.
#[global]
Hint Resolve FVars_Open_Beq : Piull.

(**
*)
Lemma FVars_Open :
forall (Q : Process)( y x i : nat),
x ∈ FVars ( {i ~> y} Q ) ->  x = y \/ x ∈ FVars ( Q ).
Proof.
  induction Q;
  intros;
  try simpl in *; try apply Union_inv in H; Piauto.
  + destruct H.
    - destruct x; simpl in *.
      * apply Singleton_inv in H.
        OrSearchRew H.
      * FVars_Open_Lt H i i0.
    - destruct y; simpl in *.
      * apply Singleton_inv in H.
        OrSearchRew H.
      * FVars_Open_Lt H i i0.
  + destruct H.
    - apply IHQ1 in H.
      destruct H; auto.
      OrSearch.
    - apply IHQ2 in H.
      destruct H; auto.
      OrSearch.
  + destruct H.
    - apply Union_inv in H.
      destruct H.
      * destruct x; simpl in *.
        ** apply Singleton_inv in H.
          rewrite H.
          OrSearch.
        ** FVars_Open_Lt H i i0.
      * destruct y; simpl in *.
        ** apply Singleton_inv in H.
          rewrite H.
          OrSearch.
        ** FVars_Open_Lt H i i0.
    - apply IHQ in H.
      destruct H; auto.
      OrSearch.
  + destruct x; simpl in *.
    - apply Singleton_inv in H.
      rewrite H.
      OrSearch.
    - FVars_Open_Lt H i i0.
  + destruct H.
    - destruct x; simpl in *.
      * apply Singleton_inv in H.
        rewrite H.
        OrSearch.
      * FVars_Open_Lt H i i0.
    - apply IHQ in H.
      destruct H; auto.
      OrSearch.
  + apply (IHQ _ _ (S i)); auto.
  + destruct H.
    - destruct x; simpl in *.
      * apply Singleton_inv in H.
        rewrite H.
        OrSearch.
      * FVars_Open_Lt H i i0.
    - apply IHQ in H.
      destruct H; auto.
      OrSearch.
  + destruct H.
    - destruct x; simpl in *.
      * apply Singleton_inv in H.
        rewrite H.
        OrSearch.
      * FVars_Open_Lt H i i0.
    - apply IHQ in H.
      destruct H; auto.
      OrSearch.
Qed.
#[global]
Hint Resolve FVars_Open : Piull.

(**
*)
Lemma FVars_Beq_Close :
forall ( Q : Process)(x x0 i : nat),
x <> x0 -> x ∈ FVars (Close_Rec i x0 Q) ->
x ∈ FVars (Q).
Proof.
  induction Q;
  intros; simpl in *;
  try apply Union_inv in H0; Piauto.
  + destruct H0.
    - destruct x;
       simpl in H0; try contradiction; auto.
      FVars_Beq_Close_Lt H0 x x1.
    - destruct y;
       simpl in H0; try contradiction; auto.
      FVars_Beq_Close_Lt H0 x2 x1.
  + destruct H0.
    - left.
      apply (IHQ1 _ x0 i); auto.
    - right.
      apply (IHQ2 _ x0 i); auto.
  + destruct H0.
    - simpl in H0.
      apply Union_inv in H0.
      destruct H0.
      * destruct x;
         simpl in H0; try contradiction; auto.
        FVars_Beq_Close_Lt H0 x x1.
      * destruct y;
         simpl in H0; try contradiction; auto.
        FVars_Beq_Close_Lt H0 x2 x1.
    - right.
      apply (IHQ x0 x1 i); auto.
  + destruct x;
     simpl in H0; try contradiction; auto.
    FVars_Beq_Close_Lt H0 x x1.
  + destruct H0.
    - destruct x;
       simpl in H0; try contradiction; auto.
      FVars_Beq_Close_Lt H0 x x1.
    - right.
      apply (IHQ x0 x1 i); auto.
  + apply (IHQ x x0 (S i)); auto.
  + destruct H0.
    - destruct x;
       simpl in H0; try contradiction; auto.
      FVars_Beq_Close_Lt H0 x x1.
    - right.
      apply (IHQ x0 x1 (S i)); auto.
  + destruct H0.
    - destruct x;
       simpl in H0; try contradiction; auto.
      FVars_Beq_Close_Lt H0 x x1.
    - right.
      apply (IHQ x0 x1 (S i)); auto.
Qed.
#[global]
Hint Resolve FVars_Beq_Close : Piull.

(**
*)
Lemma FVars_Close_NotIn :
forall ( P : Process )( x x0 i: nat),
x <> x0 -> ~ x ∈ FVars (Close_Rec i x0 P) -> ~ x ∈ FVars (P).
Proof.
  induction P; intros; simpl; unfold not; intro; apply H0; auto.
  + apply Union_inv in H1.
    destruct H1.
    - destruct x; simpl in H1; try contradiction.
      apply Singleton_inv in H1.
      rewrite <- H1 in H.
      apply beq_nat_false_inv in H.
      simpl.
      rewrite H.
      left; simpl.
      rewrite H1.
      constructor.
    - destruct y; simpl in H1; try contradiction.
      apply Singleton_inv in H1.
      rewrite <- H1 in H.
      apply beq_nat_false_inv in H.
      simpl.
      rewrite H.
      right; simpl.
      rewrite H1.
      constructor.
  + simpl in H0.
    apply No_Union_No_Each in H0.
    destruct H0 as [HA HB].
    apply Union_inv in H1.
    destruct H1.
    - apply IHP1 in HA; try contradiction; auto.
    - apply IHP2 in HB; try contradiction; auto.
  + simpl in H0.
    apply No_Union_No_Each in H0.
    destruct H0 as [HA HC].
    apply Union_inv in H1.
    destruct H1.
    - apply No_Union_No_Each in HA.
      destruct HA as [HA HB].
      apply Union_inv in H0.
      destruct H0.
      * destruct x; simpl in H0; try contradiction.
        apply Singleton_inv in H0.
        rewrite <- H0 in H.
        apply beq_nat_false_inv in H.
        simpl.
        rewrite H.
        left; left; simpl.
        rewrite H0.
        constructor.
      * destruct y; simpl in H0; try contradiction.
        apply Singleton_inv in H0.
        rewrite <- H0 in H.
        apply beq_nat_false_inv in H.
        simpl.
        rewrite H.
        left; right; simpl.
        rewrite H0.
        constructor.
    - apply IHP in HC; try contradiction; auto.
  + simpl in H0.
    destruct x; simpl in H1; try contradiction.
        apply Singleton_inv in H1.
        rewrite <- H1 in H.
        apply beq_nat_false_inv in H.
        simpl.
        rewrite H.
        simpl.
        rewrite H1.
        constructor.
  + simpl in H0.
    apply No_Union_No_Each in H0.
    destruct H0 as [HA HB].
    apply Union_inv in H1.
    destruct H1.
    - destruct x; simpl in H0; try contradiction.
      apply Singleton_inv in H0.
      rewrite <- H0 in H.
      apply beq_nat_false_inv in H.
      simpl.
      rewrite H.
      left; simpl.
      rewrite H0.
      constructor.
    - apply IHP in HB; try contradiction; auto.
  + simpl in H0.
    apply IHP in H0; auto.
    contradiction.
  + apply Union_inv in H1.
    destruct H1.
    - destruct x; simpl in H1; try contradiction.
      apply Singleton_inv in H1.
      rewrite <- H1 in H.
      apply beq_nat_false_inv in H.
      simpl.
      rewrite H.
      left; simpl.
      rewrite H1.
      constructor.
    - simpl in H0.
      apply No_Union_No_Each in H0.
      destruct H0 as [HA HB].
      apply IHP in HB; auto.
      contradiction.
  + apply Union_inv in H1.
    destruct H1.
    - destruct x; simpl in H1; try contradiction.
      apply Singleton_inv in H1.
      rewrite <- H1 in H.
      apply beq_nat_false_inv in H.
      simpl.
      rewrite H.
      left; simpl.
      rewrite H1.
      constructor.
    - simpl in H0.
      apply No_Union_No_Each in H0.
      destruct H0 as [HA HB].
      apply IHP in HB; auto.
      contradiction.
Qed.
#[global]
Hint Resolve FVars_Close_NotIn : Piull.

(**
*)
Lemma FVars_Subst :
forall ( P : Process )( x y x0 : nat ),
x ∈ FVars ({y \ x0} P) -> x = y \/ x ∈ FVars (P).
Proof.
  induction P; intros; simpl; auto.
  + simpl in H.
    apply Union_inv in H.
    destruct H.
    - destruct x; try contradiction.
      simpl in H.
      DecidSimple x x1.
      rewrite e in H.
      apply Singleton_inv in H; auto.
      rewrite n in H.
      apply Singleton_inv in H; auto.
      rewrite H.
      right; left.
      constructor.
    - destruct y; try contradiction.
      simpl in H.
      DecidSimple x2 x1.
      rewrite e in H.
      apply Singleton_inv in H; auto.
      rewrite n in H.
      apply Singleton_inv in H; auto.
      rewrite H.
      right; right.
      constructor.
  + simpl in H.
    apply Union_inv in H.
    destruct H.
    - apply IHP1 in H.
      destruct H; auto.
      OrSearch.
    - apply IHP2 in H.
      destruct H; auto.
      OrSearch.
  + simpl in H.
    apply Union_inv in H.
    destruct H.
    - apply Union_inv in H.
      destruct H.
      * destruct x; try contradiction.
        simpl in H.
        DecidSimple x x1.
        rewrite e in H.
        apply Singleton_inv in H; auto.
        rewrite n in H.
        apply Singleton_inv in H; auto.
        rewrite H.
        right; left; left.
        constructor.
      * destruct y; try contradiction.
        simpl in H.
        DecidSimple x2 x1.
        rewrite e in H.
        apply Singleton_inv in H; auto.
        rewrite n in H.
        apply Singleton_inv in H; auto.
        rewrite H.
        right; left; right.
        constructor.
    - apply IHP in H.
      destruct H; auto.
      right; right; auto.
  + simpl in H.
    destruct x; try contradiction.
    simpl in H.
    DecidSimple x x1.
    rewrite e in H.
    apply Singleton_inv in H; auto.
    rewrite n in H.
    apply Singleton_inv in H; auto.
    rewrite H.
    right.
    constructor.
  + simpl in H.
    apply Union_inv in H.
    destruct H.
    - destruct x; try contradiction.
      simpl in H.
      DecidSimple x x1.
      rewrite e in H.
      apply Singleton_inv in H; auto.
      rewrite n in H.
      apply Singleton_inv in H; auto.
      rewrite H.
      right; left.
      constructor.
    - apply IHP in H.
      destruct H; auto.
      right; right; auto.
  + simpl in H.
    apply IHP in H; auto.
  + simpl in H.
    apply Union_inv in H.
    destruct H.
    - destruct x; try contradiction.
      simpl in H.
      DecidSimple x x1.
      rewrite e in H.
      apply Singleton_inv in H; auto.
      rewrite n in H.
      apply Singleton_inv in H; auto.
      rewrite H.
      right; left.
      constructor.
    - apply IHP in H.
      destruct H; auto.
      right; right; auto.
  + simpl in H.
    apply Union_inv in H.
    destruct H.
    - destruct x; try contradiction.
      simpl in H.
      DecidSimple x x1.
      rewrite e in H.
      apply Singleton_inv in H; auto.
      rewrite n in H.
      apply Singleton_inv in H; auto.
      rewrite H.
      right; left.
      constructor.
    - apply IHP in H.
      destruct H; auto.
      OrSearch.
Qed.
#[global]
Hint Resolve FVars_Subst : Piull.

(**
*)
Lemma Close_FVars_Beq:
forall (P : Process) (u x i : nat),
u <> x -> u ∈ FVars (Close_Rec i x P) -> u ∈ FVars P.
Proof.
  intro.
  induction P; intros; Piauto.
  + simpl in H0.
    destruct H0.
    - destruct x; try contradiction.
      simpl in H0.
      DecidSimple x x0.
      * rewrite e in H0.
        simpl in H0.
        contradiction.
      * rewrite n in H0.
        simpl in H0.
        inversions H0.
        OrSearch.
    - destruct y; try contradiction.
      simpl in H0.
      DecidSimple x2 x0.
      * rewrite e in H0.
        simpl in H0.
        contradiction.
      * rewrite n in H0.
        simpl in H0.
        inversions H0.
        OrSearch.
  + simpl in H0. simpl.
    inversions H0.
    - left.
      apply (IHP1 u x i); Piauto.
    - right.
      apply (IHP2 u x i); Piauto.
  + simpl in H0.
    destruct H0.
    - destruct H0.
      * destruct x; try contradiction.
        simpl in H0.
        DecidSimple x x0.
        ** rewrite e in H0.
           simpl in H0.
           contradiction.
        ** rewrite n in H0.
           simpl in H0.
           inversions H0.
           OrSearch.
      * destruct y; try contradiction.
        simpl in H0.
        DecidSimple x2 x0.
        ** rewrite e in H0.
           simpl in H0.
           contradiction.
        ** rewrite n in H0.
           simpl in H0.
           inversions H0.
           OrSearch.
    - simpl. right.
      apply (IHP x1 x0 i); Piauto.
  + simpl in H0.
    destruct x; try contradiction.
    simpl in H0.
    DecidSimple x x0.
    - rewrite e in H0.
      simpl in H0.
      contradiction.
    - rewrite n in H0.
      simpl in H0.
      inversions H0.
      OrSearch.
  + simpl in H0.
    apply Union_inv in H0.
    destruct H0.
    - destruct x; try contradiction.
      simpl in H0.
      DecidSimple x x0.
      * rewrite e in H0.
        simpl in H0.
        inversions H0.
      * rewrite n in H0.
        simpl in H0.
        inversions H0.
        OrSearch.
    - specialize (IHP _ _ i H H0).
      OrSearch.
  + simpl in H0.
    simpl.
    apply (IHP u x (S i)); Piauto.
  + simpl in H0.
    apply Union_inv in H0.
    destruct H0.
    - destruct x; try contradiction.
      simpl in H0.
      DecidSimple x x0.
      * rewrite e in H0.
        inversions H0.
      * rewrite n in H0.
        inversions H0.
        OrSearch.
    - simpl in H0.
      specialize (IHP _ _ _ H H0).
      OrSearch.
  + simpl in H0.
    apply Union_inv in H0.
    destruct H0.
    - destruct x; try contradiction.
      simpl in H0.
      DecidSimple x x0.
      * rewrite e in H0.
        inversions H0.
      * rewrite n in H0.
        inversions H0.
        OrSearch.
    - simpl in H0.
      specialize (IHP _ _ _ H H0).
      OrSearch.
Qed.
#[global]
Hint Resolve Close_FVars_Beq : Piull.

(**
*)
Lemma FVars_Subst_In :
forall ( P : Process )( x y x0 : nat ),
x0 ∈ FVars P -> x ∈ FVars ({y \ x0} P) -> (x = y \/ (x ∈ FVars (P) /\ x <> x0)).
Proof.
  intros.
  DecidSimple x y.
  DecidSimple x x0.
  apply beq_nat_false in n.
  + apply beq_nat_true in e.
    rewrite e in *.
    apply After_Subst_No_FVar in H0; Piauto.
  + apply FVars_Subst in H0.
    destruct H0; Piauto.
    apply beq_nat_false in n0.
    right; constructor; Piauto.
Qed.
#[global]
Hint Resolve FVars_Subst_In : Piull.

(**
*)
Lemma FVars_Res_Neg :
forall ( P : Process )( x : nat ),
~ x ∈ FVars (ν P) <-> ~ x ∈ FVars P.
Proof.
  constructor; Piauto.
Qed.
#[global]
Hint Resolve FVars_Res_Neg : Piull.

(**
*)
Lemma FVars_Res :
forall ( P : Process )( x : nat ),
x ∈ FVars (ν P) <-> x ∈ FVars P.
Proof.
  constructor; Piauto.
Qed.
#[global]
Hint Resolve FVars_Res : Piull.

(**
*)
Lemma NFVar_Close_Names :
forall (z : Name)(x i : nat ),
x ∈ FVars_Name (Close_Name i x z) -> False.
Proof.
  intros.
  destruct z; simpl in H; try contradiction.
  DecidSimple x0 x.
  + rewrite e in H.
    simpl in H.
    contradiction.
  + rewrite n in H.
    simpl in H.
    apply Singleton_inv in H.
    apply beq_nat_false in n.
    contradiction.
Qed.
#[global]
Hint Resolve NFVar_Close_Names : Piull.

(**
*)
Lemma NFVar_Close_Cases :
forall (P : Process )( x u : nat),
~ x ∈ FVars (Close u P) -> x = u \/ ( x <> u /\ ~ x ∈ FVars P).
Proof.
  intros.
  DecidSimple x u.
  apply beq_nat_false in n.
  right.
  constructor; Piauto.
  unfold not.
  intros.
  Piauto.
  specialize (FVars_Close_Beq  P x u 0 n H0) as Hx.
  Piauto.
Qed.
#[global]
Hint Resolve NFVar_Close_Cases : Piull.

(**
*)
Lemma NFVar_Close :
forall ( P : Process )( i x : nat ),
~ x ∈ FVars (Close_Rec i x P).
Proof.
  unfold not.
  induction P; simpl; intros; try inversions H; ePiauto.
  inversions H0; ePiauto.
Qed.
#[global]
Hint Resolve NFVar_Close : Piull.

(**
*)
Lemma Close_Parallel :
forall ( u : nat)(P Q : Process),
Close u (P ↓ Q) = (Close u P) ↓ (Close u Q).
Proof.
  Piauto.
Qed.
#[global]
Hint Resolve Close_Parallel : Piull.

(** FVars_Close_NotIn
*)
Lemma FVars_Reduction_Neg :
forall ( P Q : Process )( x : nat),
~ x ∈ FVars P -> P --> Q -> ~ x ∈ FVars Q.
Proof.
  intros.
  induction H0.
  + apply -> FVars_Res_Neg in H.
    specialize (NFVar_Close_Cases _ x x0 H) as Ht.
    destruct Ht; try rewrite H5; Piauto.

    destruct H5.
    apply No_FVars_Parallel in H6.
    destruct H6 as [HA HB].
    unfold not.
    intros.
    apply FVars_Subst in H6.
    destruct H6; try contradiction.
    rewrite H6 in HB.
    simpl in HB.
    apply No_Union_No_Each in HB.
    destruct HB.
    apply H8.
    constructor.
  + apply -> FVars_Res_Neg in H.
    specialize (NFVar_Close_Cases _ x x0 H) as Ht.
    destruct Ht; try rewrite H5; Piauto.

    destruct H5.
    apply No_FVars_Parallel in H6.
    destruct H6 as [HA HB].
    unfold not.
    intros.
    apply FVars_Subst in H6.
    destruct H6; try contradiction.
    rewrite H6 in HB.
    simpl in HB.
    apply No_Union_No_Each in HB.
    destruct HB.
    apply H7.
    constructor.
  + apply -> FVars_Res_Neg in H.
    specialize (NFVar_Close_Cases _ x x0 H) as Ht.
    destruct Ht; try rewrite H5; Piauto.

    destruct H5.
    apply No_FVars_Parallel in H6.
    destruct H6 as [HA HB].
    unfold not.
    intros.
    apply FVars_Subst in H6.
    destruct H6; try contradiction.
    rewrite H6 in HA.
    simpl in HA.
    apply No_Union_No_Each in HA.
    destruct HA.
    apply H7.
    constructor.
  + apply -> FVars_Res_Neg in H.
    specialize (NFVar_Close_Cases _ x x0 H) as Ht.
    destruct Ht; try rewrite H5; Piauto.

    destruct H5.
    apply No_FVars_Parallel in H6.
    destruct H6 as [HA HB].
    unfold not.
    intros.
    apply FVars_Subst in H6.
    destruct H6; try contradiction.
    rewrite H6 in HA.
    simpl in HA.
    apply No_Union_No_Each in HA.
    destruct HA.
    apply H8.
    constructor.
  + apply -> FVars_Res_Neg in H.
    specialize (NFVar_Close_Cases _ x x0 H) as Ht.
    destruct Ht; try rewrite H4; Piauto.

    destruct H4.
    apply No_FVars_Parallel in H5.
    destruct H5 as [HA HB].
    unfold not in *.
    intros.
    apply HB.
    simpl.
    OrSearch.
  + apply -> FVars_Res_Neg in H.
    specialize (NFVar_Close_Cases _ x x0 H) as Ht.
    destruct Ht; try rewrite H4; Piauto.

    destruct H4.
    apply No_FVars_Parallel in H5.
    destruct H5 as [HA HB].
    unfold not in *.
    intros.
    apply HA.
    simpl.
    OrSearch.
  + apply -> FVars_Res_Neg in H.
    specialize (NFVar_Close_Cases _ x u H) as Ht.
    destruct Ht.
    - rewrite H9 in *.
      apply NFVar_Close.
    - destruct H9.
      apply No_FVars_Parallel in H10.
      destruct H10.
      rewrite Close_Parallel.
      unfold not.
      intros.
      simpl in H12.
      apply Union_inv in H12.
      destruct H12.
      * apply Union_inv in H12.
        destruct H12.
        ++ DecidSimple u u.
           rewrite e in H12.
           inversions H12.
        ++ apply H10.
           apply Close_FVars_Beq in H12; Piauto.
           OrSearch.
      * apply Union_inv in H12.
        destruct H12.
        ++ apply Close_FVars_Beq in H12; Piauto.
           DecidSimple x y.
           -- apply beq_nat_true in e.
              subst.
              apply NFVar_Close in H12; auto.
           -- apply H11.
              OrSearch.
        ++ apply Close_FVars_Beq in H12; Piauto.
           DecidSimple x y.
           -- apply beq_nat_true in e.
              subst.
              apply NFVar_Close in H12; auto.
           -- apply beq_nat_false in n.
              apply FVars_Beq_Close in H12; Piauto.
              apply FVars_Open_Beq in H12; Piauto.
              apply H10.
              OrSearch.
  + apply -> FVars_Res_Neg in H.
    specialize (NFVar_Close_Cases _ x u H) as Ht.
    destruct Ht.
    - rewrite H9 in *.
      apply NFVar_Close.
    - destruct H9.
      apply No_FVars_Parallel in H10.
      destruct H10.
      rewrite Close_Parallel.
      unfold not.
      intros.
      simpl in H12.
      apply Union_inv in H12.
      destruct H12.
      * apply Union_inv in H12.
        destruct H12.
        ++ DecidSimple u u.
           rewrite e in H12.
           inversions H12.
        ++ apply H10.
           apply Close_FVars_Beq in H12; Piauto.
           OrSearch.
      * apply Union_inv in H12.
        destruct H12.
        ++ apply Close_FVars_Beq in H12; Piauto.
           DecidSimple x y.
           -- apply beq_nat_true in e.
              subst.
              apply NFVar_Close in H12; auto.
           -- apply beq_nat_false in n.
              apply FVars_Beq_Close in H12; Piauto.
              apply FVars_Open_Beq in H12; Piauto.
              apply H10.
              OrSearch.
        ++ apply Close_FVars_Beq in H12; Piauto.
           DecidSimple x y.
           -- apply beq_nat_true in e.
              subst.
              apply NFVar_Close in H12; auto.
           -- apply H11.
              OrSearch.
  + apply -> FVars_Res_Neg in H.
    specialize (NFVar_Close_Cases _ x x0 H) as Ht.
    destruct Ht.
    - subst.
      unfold not in *.
      intros.
      apply Close_FVars_Beq in H11; Piauto.
      simpl in H11.
      apply Union_inv in H11.
      destruct H11; Piauto.
      apply Union_inv in H11.
      destruct H11.
      apply (NFVar_Close (P ^ y) 0 x0); Piauto.
      apply (NFVar_Close R 0 x0); Piauto.
    - destruct H11.
      apply No_FVars_Parallel in H12.
      destruct H12.
      apply -> FVars_Res_Neg in H13.
      specialize (NFVar_Close_Cases _ x y H13) as Ht.
      apply FVars_Res_Neg.
      destruct Ht.
      * subst.
        apply NFVar_Close.
      * destruct H14.
        unfold not.
        intros.
        apply Close_FVars_Beq in H16; Piauto.
        simpl in H16.
        apply Union_inv in H16.
        destruct H16.
        ++ apply Union_inv in H16.
           destruct H16.
           apply Close_FVars_Beq in H16; Piauto.
           apply FVars_Open_Beq in H16; Piauto.
           apply H12; OrSearch.
           apply Close_FVars_Beq in H16; Piauto.
           apply H15; OrSearch.
        ++ apply H15; OrSearch.
  + apply -> FVars_Res_Neg in H.
    specialize (NFVar_Close_Cases _ x x0 H) as Ht.
    destruct Ht.
    - rewrite H10 in *.
      apply NFVar_Close.
    - destruct H10.
      apply No_FVars_Parallel in H11.
      destruct H11.
      apply -> FVars_Res_Neg in H11.
      specialize (NFVar_Close_Cases _ x y H11) as Ht.
      apply FVars_Res_Neg.
      unfold not.
      intros.
      apply Close_FVars_Beq in H13; Piauto.
      destruct Ht.
      * subst.
        simpl in H13.
        apply Union_inv in H13.
        destruct H13; Piauto.
        apply Union_inv in H13.
        destruct H13;
        apply NFVar_Close in H13; Piauto.
      * destruct H14.
        destruct H13; Piauto.
        apply H15; OrSearch.
        apply Close_FVars_Beq in H13; Piauto.
        simpl in H13.
        apply Union_inv in H13.
        destruct H13.
        apply H15; OrSearch.
        apply FVars_Open_Beq in H13; Piauto.
        apply H12; OrSearch.
Qed.
#[global]
Hint Resolve FVars_Reduction_Neg : Piull.

(**
*)
Lemma In_FVars_Res :
forall ( P : Process )( x u  : nat ),
x ∈ FVars (ν Close u P) -> x ∈ FVars P /\ x <> u.
Proof.
  intros.
  DecidSimple x u.
  + apply beq_nat_true in e.
    subst.
    apply NFVar_Close in H.
    contradiction.
  + apply beq_nat_false in n.
    specialize (Close_FVars_Beq P x u 0 n H) as Hx.
    Piauto.
Qed.
#[global]
Hint Resolve In_FVars_Res : Piull.

(**
*)
Lemma Close_Parallel_NFVar :
forall ( P Q : Process )( y : nat ),
~ y ∈ FVars P -> P ↓ Close y Q = Close y (P↓Q).
Proof.
  intros.
  unfold Close.
  simpl.
  rewrite (Close_NoFVar_Eq P y 0); Piauto.
Qed.
#[global]
Hint Resolve Close_Parallel_NFVar : Piull.

(**
*)
Lemma Rep_Input_NFVar :
forall ( P : Process )( u y : nat),
y <> u -> ~ y ∈ FVars P -> ~ y ∈ FVars (FName u !· P).
Proof.
  unfold not.
  intros.
  destruct H1; Piauto.
  apply Singleton_inv in H1.
  lia.
Qed.
#[global]
Hint Resolve Rep_Input_NFVar : Piull.

(** FVars_Close_NotIn
*)
Lemma FVars_Reduction_Inv :
forall ( P Q : Process )( x : nat),
x ∈ FVars Q -> P --> Q -> x ∈ FVars P.
Proof.
  intros.
  induction H0.
  + specialize ( FVars_Subst_In _ _ _ _ H4 H) as Hx.
    destruct Hx.
    - DecidSimple y x0.
      simpl.
      rewrite n.
      rewrite H5.
      do 2 right.
      constructor.
    - destruct H5.
      apply FVars_Res.
      apply FVars_Close_Beq; Piauto.
      OrSearch.
  + specialize ( FVars_Subst_In _ _ _ _ H4 H) as Hx.
    destruct Hx.
    - DecidSimple y x0.
      simpl.
      rewrite n.
      rewrite H5.
      right. left.
      constructor.
    - destruct H5.
      apply FVars_Res.
      apply FVars_Close_Beq; Piauto.
      OrSearch.
  + specialize ( FVars_Subst_In _ _ _ _ H4 H) as Hx.
    destruct Hx.
    - DecidSimple y x0.
      simpl.
      rewrite n.
      subst.
      do 2 left.
      constructor.
    - destruct H5.
      apply FVars_Res.
      apply FVars_Close_Beq; Piauto.
      OrSearch.
  + specialize ( FVars_Subst_In _ _ _ _ H4 H) as Hx.
    destruct Hx.
    - DecidSimple y x0.
      simpl.
      rewrite n.
      subst.
      left.
      right.
      constructor.
    - destruct H5.
      apply FVars_Res.
      apply FVars_Close_Beq; Piauto.
      OrSearch.
  + DecidSimple x x0.
    apply beq_nat_true in e.
    rewrite e in H.
    contradiction.
    apply beq_nat_false in  n.
    apply FVars_Res.
    apply FVars_Close_Beq; Piauto.
    OrSearch.
  + DecidSimple x x0.
    apply beq_nat_true in e.
    rewrite e in H.
    contradiction.
    apply beq_nat_false in  n.
    apply FVars_Res.
    apply FVars_Close_Beq; Piauto.
    OrSearch.
  + apply -> FVars_Res in H.
    DecidSimple x u.
    apply beq_nat_true in e.
    rewrite e in *.
    apply NFVar_Close in H.
    contradiction.

    apply beq_nat_false in n.
    apply FVars_Close_Beq; Piauto.
    apply FVars_Beq_Close in H; Piauto.
    destruct H.
    - destruct H.
      * simpl in H.
        apply Singleton_inv in H.
        lia.
      * OrSearch.
    - apply -> FVars_Res in H.
      DecidSimple x y.
      apply beq_nat_true in e.
      rewrite e in H.
      apply NFVar_Close in H.
      contradiction.

      apply beq_nat_false in n0.
      inversions H0.
      rewrite (Cong_FVars
        ((FName u !· P) ↓ (ν Close y (FName u « FName y »· Q)) )
        (ν ((FName u !· P) ↓ Close y (FName u « FName y »· Q)) ) ); Piauto.
      rewrite Close_Parallel_NFVar; Piauto.
      apply FVars_Close_Beq; Piauto.
      apply FVars_Beq_Close in H; Piauto.
      destruct H.
      * OrSearch.
      * apply FVars_Open_Beq in H; Piauto.
        OrSearch.
  + apply -> FVars_Res in H.
    DecidSimple x u.
    apply beq_nat_true in e.
    rewrite e in *.
    apply NFVar_Close in H.
    contradiction.

    apply beq_nat_false in n.
    apply FVars_Close_Beq; Piauto.
    apply FVars_Beq_Close in H; Piauto.
    destruct H.
    - destruct H.
      * simpl in H.
        apply Singleton_inv in H.
        lia.
      * OrSearch.
    - apply -> FVars_Res in H.
      DecidSimple x y.
      apply beq_nat_true in e.
      rewrite e in H.
      apply NFVar_Close in H.
      contradiction.

      apply beq_nat_false in n0.
      inversions H0.
      rewrite (Cong_FVars
        ((FName u !· P) ↓ (ν Close y (FName u « FName y »· Q)) )
        (ν ((FName u !· P) ↓ Close y (FName u « FName y »· Q)) ) ); Piauto.
      rewrite Close_Parallel_NFVar; Piauto.
      apply FVars_Close_Beq; Piauto.
      apply FVars_Beq_Close in H; Piauto.
      destruct H.
      * apply FVars_Open_Beq in H; Piauto.
        OrSearch.
      * OrSearch.
  + apply -> FVars_Res in H.
    DecidSimple x y.
    apply beq_nat_true in e.
    rewrite e in *.
    apply NFVar_Close in H.
    contradiction.

    apply beq_nat_false in n.
    apply FVars_Beq_Close in H; Piauto.
    destruct H.
    - apply -> FVars_Res in H.
      DecidSimple x x0.
      apply beq_nat_true in e.
      rewrite e in H.
      apply NFVar_Close in H.
      contradiction.

      apply beq_nat_false in n0.
      apply FVars_Beq_Close in H; Piauto.
      destruct H.
      * apply FVars_Open_Beq in H; Piauto.
        OrSearch.
      * OrSearch.

    - DecidSimple x x0.
      apply beq_nat_true in e.
      subst.
      contradiction.

      apply beq_nat_false in n0.
      right.
      apply FVars_Close_Beq; Piauto.
      OrSearch.

  + apply -> FVars_Res in H.
    DecidSimple x x0.
    apply beq_nat_true in e.
    rewrite e in *.
    apply NFVar_Close in H.
    contradiction.

    apply beq_nat_false in n.
    apply FVars_Close_Beq; Piauto.
    apply FVars_Beq_Close in H; Piauto.
    destruct H.
    - DecidSimple x y.
      apply beq_nat_true in e.
      subst.
      contradiction.

      apply beq_nat_false in n0.
      left.
      apply FVars_Close_Beq; Piauto.
      OrSearch.
    - apply -> FVars_Res in H.
      DecidSimple x y.
      apply beq_nat_true in e.
      rewrite e in H.
      apply NFVar_Close in H.
      contradiction.

      apply beq_nat_false in n0.
      inversions H0.
      apply FVars_Beq_Close in H; Piauto.
      destruct H.
      * OrSearch.
      * apply FVars_Open_Beq in H; Piauto.
        OrSearch.
Qed.
#[global]
Hint Resolve FVars_Reduction_Inv : Piull.

(**
*)
Lemma Not_FVar_Subst :
forall ( x w z : nat )( P : Process ),
x <> w -> ~ x ∈ FVars (P) ->
~ x ∈ FVars ({w \ z} P).
Proof.
  unfold not.
  intros.
  apply FVars_Subst in H1.
  destruct H1; Piauto.
Qed.
#[global]
Hint Resolve Not_FVar_Subst : Piull.

author: cigarcial

repo: Tmcod

save_path: github-repos/coq/cigarcial-Tmcod


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

Derive Show for natural.

              Derive Arbitrary for natural.

              Instance Dec_Eq_natural : Dec_Eq natural.

              Proof. dec_eq. Qed.
Derive Show for lst.

              Derive Arbitrary for lst.

              Instance Dec_Eq_lst : Dec_Eq lst.

              Proof. dec_eq. Qed.

Lemma lfind_hyp_test : (@eq lst (append (Cons (Zero) (Nil)) (append (Nil) (Nil))) (append (append (Cons (Zero) (Nil)) (Nil)) (Nil))).
Admitted.
QuickChick lfind_hyp_test.

author: yalhessi

repo: lemmaranker

save_path: github-repos/coq/yalhessi-lemmaranker


text:
Require Export DecidableEnumerable.

(** * Dialogue Semantics *)

(** ** Generalized Intuitionistic E-Completeness *)

Definition ocons X (o : option X) A :=
  match o with
  | Some a => a :: A
  | None => A
  end.
Infix "o::" := ocons (at level 55).

Lemma ocons_sub X (a : option X) A B :
  A <<= B -> a o:: A <<= a o:: B.
Proof.
  intros H. destruct a; cbn.
  - intros y []; subst; intuition.
  - assumption.
Qed.

(** *** Generalized Intuitionistic E-Dialogues *)

Class rule_set (f : Type) :=
  {
    atomic : f -> Prop ;
    attack : f -> option f -> Type ;
    defense : forall phi adm, attack phi adm -> f -> Prop ;
    dec_f : eq_dec f
  }.

Definition opred X (p : X -> Prop) (o : option X) : Prop :=
  forall x, o = Some x -> p x.

Section EGame.
  Variable f : Type.
  Variable R : rule_set f.

  Definition justified A phi := atomic phi -> phi el A.

  Lemma justified_weak A B phi :
    justified A phi -> A <<= B -> justified B phi.
  Proof.
    intros Hjust Hsub Hin. intuition.
  Qed.

  Inductive challenge : Type :=
    C phi adm : attack phi adm -> challenge.

  Inductive opening phi : list f -> challenge -> Type :=
    OP (H : justified nil phi) adm (atk : attack phi adm) : opening phi (adm o:: nil) (C atk).

  Inductive epmove : list f -> challenge -> Type :=
  | EPAtk A c phi adm : phi el A -> opred (justified A) adm -> attack phi adm -> epmove A c
  | EPDef A phi adm (atk : attack phi adm) psi : justified A psi -> defense atk psi -> epmove A (C atk).

  Inductive eomove : forall A c,  epmove A c -> list f -> challenge -> Type :=
  | EODef A c phi adm H H' (atk : attack phi adm) psi :
      defense atk psi -> @eomove A _ (EPAtk c H H' atk) (psi :: A) c
  | EOCounter A c phi psi H H' (atk : attack phi (Some psi)) adm (atk' : attack psi adm) :
      @eomove A _ (EPAtk c H H' atk) (adm o:: A) (C atk')
  | EOAtk A phi adm (atk : attack phi adm) psi (H : justified A psi) (def : defense atk psi) adm'
         (atk' : attack psi adm') :
      eomove (EPDef H def) (adm' o:: A) (C atk').

  Inductive ewin_strat A c : Prop :=
    EWS (pm : epmove A c) : (forall A' c', eomove pm A' c' -> ewin_strat A' c') -> ewin_strat A c.

  Definition evalid phi :=
    justified nil phi /\ forall A c, opening phi A c -> ewin_strat A c.
End EGame.

(** *** Dialogical Sequent Calculus *)

Section LJD.
  Variable f : Type.
  Variable R : rule_set f.

  Inductive Dprv (A : list f) (T : f -> Prop): Prop :=
    Def phi :
      T phi ->
      justified _ A phi ->
      (forall adm (atk : attack phi adm), Dprv (adm o:: A) (defense atk)) ->
      Dprv A T
  | Att psi adm (atk : attack psi adm) :
      psi el A ->
      (forall chi, defense atk chi -> Dprv (chi :: A) T) ->
      opred (fun a => justified _ A a) adm ->
      opred (fun a => forall adm' (atk' : attack a adm'), Dprv (adm' o:: A) (defense atk')) adm ->
      Dprv A T.
  Notation "A '⊢D' T" := (Dprv A T) (at level 30).

(** *** Soundness and Completeness *)

  Lemma Dprv_ewin A T :
    A ⊢D T -> forall phi adm (atk : attack phi adm), (forall psi, T psi -> defense atk psi) -> ewin_strat A (C atk).
  Proof.
    induction 1.
    - intros psi adm atk Hdef. apply EWS with (pm := (EPDef H0 (Hdef _ H))).
      intros A' c'. inversion 1; subst. now apply (H2 adm' atk').
    - intros xi adm' atk' Hdef. apply EWS with (pm := (EPAtk _ H H2 atk)).
        intros A' c'. intros Hinv. revert H1 H4. inversion Hinv; subst; intros IH IH'.
        (* Opponent defends *)
        * enough (atk1 = atk) as -> by now apply IH.
          do 2 eapply Eqdep_dec.inj_pair2_eq_dec in H10.
          assumption. apply option_eq_dec. all: exact dec_f.
        (* Opponent countered  *)
        * now apply (IH' psi0 eq_refl adm0 atk'0).
  Qed.

  Lemma esoundsess phi :
    nil ⊢D (fun psi => psi = phi) -> evalid _ phi.
  Proof.
    inversion 1; subst.
    - split; [exact H1 |]; intros A c [Hjust adm atk].
      specialize (H2 adm atk); now apply (Dprv_ewin H2).
    - contradiction H0.
  Qed.

  Lemma ewin_Dprv A c :
    ewin_strat A c -> match c with C atk => A ⊢D (defense atk) end.
  Proof.
    induction 1. revert H H0; destruct pm; intros Hwin IH.
      (* Player attacks *)
    - destruct c as [psi adm' atk]. apply (@Att _ _ phi adm a); intuition.
      + apply (IH _ (C atk)). apply (EODef (C atk) i o H).
      + intros chi -> adm'' atk'. apply (IH _ (C atk')). apply EOCounter.
      (* Player defends *)
    - apply (@Def _ _ psi); intuition. apply (IH _ (C atk0)). apply EOAtk.
  Qed.

  Lemma ecompleteness phi :
    evalid _ phi -> nil ⊢D (fun psi => psi = phi).
  Proof.
    intros [Hjust Hwin]. apply (@Def _ _ phi); intuition.
    specialize (Hwin _ _ (OP Hjust atk)).
    apply (ewin_Dprv Hwin).
  Qed.

  Lemma Dprv_weak A B (T T' : f -> Prop) :
    Dprv A T -> A <<= B -> (forall phi, T phi -> T' phi) -> Dprv B T'.
  Proof.
    intros H; revert T' B; induction H; intros T' B Hsub Himp.
    - apply (Def (Himp phi H)). now apply (justified_weak H0).
      intros. apply (H2 adm atk); eauto using ocons_sub.
    - apply (@Att _ _ _ _ atk). now apply Hsub.
      intros. apply (H1 chi). assumption. intuition.
      assumption. unfold opred. eauto using justified_weak.
      intros a Ha adm' atk'. apply (H4 _ Ha adm' atk'); eauto using ocons_sub.
  Qed.

  Lemma Dprv_defend A T phi :
    Dprv A T -> (forall psi, T psi -> psi = phi) -> forall adm (atk : attack phi adm), Dprv (adm o:: A) (defense atk).
  Proof.
    induction 1; intros HT adm' atk'.
    - rewrite (HT phi0 H) in *. apply H1.
    - apply Att with (atk := atk).
      + destruct adm'; cbn; intuition.
      + intros chi Hchi. apply (Dprv_weak (H1 chi Hchi HT adm' atk')).
        * destruct adm'; cbn; intuition.
        * intuition.
      + intros ? ->. apply (justified_weak (H2 x eq_refl)).
        destruct adm'; cbn; intuition.
      + intros ? -> adm1 atk1. apply (Dprv_weak (H3 x eq_refl adm1 atk1)).
        destruct adm1, adm'; cbn; intuition. intuition.
  Qed.

  Lemma Dprv_exp A T :
    Dprv A T -> (forall phi, ~ T phi) -> forall T', Dprv A T'.
  Proof.
    intros Hprv Hep T'. apply (Dprv_weak Hprv); firstorder.
  Qed.

  Lemma Dprv_echo (Q : f -> f -> Prop) phi :
    well_founded Q ->
    (forall phi adm (atk : attack phi adm), opred (fun a => Q a phi) adm /\ forall chi, defense atk chi -> Q chi phi) ->
    forall A, phi el A -> forall adm (atk : attack phi adm), Dprv (adm o:: A) (defense atk).
  Proof.
    intros Hwf Hdes. induction (Hwf phi) as [phi H IH]. intros A Hel.
    - intros adm atk. apply Att with (atk := atk); destruct (Hdes phi adm atk) as (Hadm & Hdefs).
      + destruct adm; cbn; intuition.
      + intros chi Hdef. apply Def with (phi := chi); unfold justified; intuition.
      + intros ? -> _; cbn; intuition.
      + intros ? -> adm' atk'; cbn. apply (IH x (Hadm x eq_refl)). intuition.
  Qed.

  Lemma Dprv_ax A (T : f -> Prop) (Q : f -> f -> Prop) phi :
    well_founded Q ->
    (forall phi adm (atk : attack phi adm), opred (fun a => Q a phi) adm /\ forall chi, defense atk chi -> Q chi phi) ->
    phi el A -> T phi -> Dprv A T.
  Proof.
    intros Hwf Hdes Hin HT. apply Def with (phi := phi); unfold justified; eauto using Dprv_echo.
  Qed.

  Lemma Dprv_just A T T' phi :
    Dprv A T -> (forall psi, T psi -> psi = phi) -> (forall B, A <<= B -> justified _ B phi -> Dprv B T') -> Dprv A T'.
  Proof.
    induction 1; intros HT HT'.
    - rewrite (HT _ H) in *; apply (HT' A); intuition.
    - apply Att with (atk := atk); intuition.
      apply H1. assumption. apply HT. intros. apply HT'; firstorder.
  Qed.

End LJD.
Notation "A '⊢D' T" := (Dprv _ A T) (at level 30).

(** ** Generalized Intuitionistic D-Completeness *)

(** *** Generalized Intuitionistic D-Dialogues *)

Section DGame.
  Variable f : Type.
  Variable R : rule_set f.

  Definition dstate : Type := list f * list (challenge _) * list f * list (challenge _).
  Inductive dpmove : dstate -> dstate -> Type :=
  | DPAtk pA pC oA oC phi adm (atk : attack phi adm) :
      phi el oA -> opred (justified _ oA) adm -> dpmove (pA, pC, oA, oC) (adm o:: pA, pC, oA, C atk :: oC)
  | DPDef pA pC oA oC phi adm (atk : attack phi adm) psi :
      justified _ oA psi -> defense atk psi -> dpmove (pA, C atk :: pC, oA, oC) (psi :: pA, pC, oA, oC).

  Inductive domove : dstate -> dstate -> Type :=
  | DOAtk pA pA' pC oA oC phi adm (atk : attack phi adm) :
      domove (pA ++ phi :: pA', pC, oA, oC) (pA ++ pA', C atk :: pC, adm o:: oA, oC)
  | DODef pA pC oA oC phi adm (atk : attack phi adm) psi :
      defense atk psi -> domove (pA, pC, oA, C atk :: oC) (pA, pC, psi :: oA, oC).

  Inductive dwin_strat s : Prop :=
    DWS s' : dpmove s s' -> (forall s'', domove s' s'' -> dwin_strat s'') -> dwin_strat s.

  Definition dvalid phi :=
    justified _ nil phi /\ forall A c, opening phi A c -> dwin_strat (nil, c :: nil, A, nil).

  Definition dwin_Dprv_embed (s : dstate) :=
    match s with
    | (_, C atk :: _, A, _) => A ⊢D (defense atk)
    | (_, nil, _, _) => True
    end.
  Lemma dwin_Dprv s :
    dwin_strat s -> dwin_Dprv_embed s.
  Proof.
    induction 1. revert H H0; destruct X; intros Hwin IH.
      (* Player attacks *)
    - destruct pC as [| [psi adm' atk'] pC]; [exact I |]; cbn.
      apply (@Att _ _ _ _ phi adm atk); intuition.
      + apply (IH (adm o:: pA, C atk' :: pC, chi :: oA, oC)). apply (DODef _ _ _ _  H).
      + intros chi -> adm'' atk''. apply (IH (pA, C atk'' :: C atk' :: pC, adm'' o:: oA, C atk :: oC)).
        cbn. apply (DOAtk nil pA _ _ _ atk'').
      (* Player defends *)
    - apply (@Def _ _ _ _ psi); intuition. apply (IH (pA, C atk0 :: pC, adm0 o:: oA, oC)).
      apply (DOAtk nil pA _ _ _ atk0).
  Qed.

  Lemma dcompleteness phi :
    dvalid phi -> nil ⊢D (fun psi => psi = phi).
  Proof.
    intros [Hjust Hwin]. apply (@Def _ _ _ _ phi); intuition.
    specialize (Hwin _ _ (OP Hjust atk)). apply (dwin_Dprv Hwin).
  Qed.

  Lemma split_right (X Y : Type) (A : list (X * Y)) b (B : list X) (C : list Y) :
    split A = (b :: B, C) -> exists A' c C', A = (b, c) :: A' /\ C = c :: C'.
  Proof.
    destruct A as [| [b' c] A']; cbn; try discriminate. destruct (split A'), C as [| c' C']; cbn; try discriminate.
    intros [= -> -> -> ->]. exists A'. exists c'. now exists C'.
  Qed.
End DGame.

(** *** Soundness and Completeness **)

Section SGame.
  Variable f : Type.
  Variable R : rule_set f.

  Definition deferred : Type := challenge _ * challenge _.
  Definition sstate : Type := list f * list f * list deferred.

  Inductive spmove : sstate -> challenge _ -> sstate -> Type :=
  | SPAtk pA oA ds c phi adm (atk : attack phi adm) :
      phi el oA -> opred (justified _ oA) adm -> spmove (pA, oA, ds) c (adm o:: pA, oA, (C atk, c) :: ds)
  | SPDef pA oA ds phi adm (atk : attack phi adm) psi :
      defense atk psi -> justified _ oA psi -> spmove (pA, oA, ds) (C atk) (psi :: pA, oA, ds).

  Inductive somove : sstate -> sstate -> challenge _ -> Type :=
  | SODef pA oA ds c phi adm (atk : attack phi adm) psi :
      defense atk psi -> somove (pA, oA, (C atk, c) :: ds) (pA, psi :: oA, ds) c
  | SOAtk pA phi pA' oA ds adm (atk : attack phi adm) :
      somove (pA ++ phi :: pA', oA, ds) (pA ++ pA', adm o:: oA, ds) (C atk).

  Inductive swin_strat s c : Prop :=
    SWS s' : spmove s c s' -> (forall s'' c', somove s' s'' c' -> swin_strat s'' c') -> swin_strat s c.

  Definition svalid phi :=
    justified _ nil phi /\ forall A c, opening phi A c -> swin_strat (nil, A, nil) c.

  Definition swin_dwin_embed s c :=
    match s with
    | (pA, oA, ds) => match split ds with (oC, pC) => dwin_strat (pA, c :: pC, oA, oC) end
    end.
  Lemma swin_dwin s c :
    swin_strat s c -> swin_dwin_embed s c.
  Proof.
    induction 1. inversion X; subst; cbn; destruct (split ds) as [oC pC] eqn:Hds.
    (* Player attacks *)
    - apply (DWS (DPAtk pA (c :: pC) oC atk H1 H2)).
      intros s''. inversion 1; subst.
      (* Opponent attacks *)
      + rewrite <- H4 in H0. specialize (H0 (pA0 ++ pA', adm0 o:: oA, (C atk, c) :: ds) (C atk0)).
        specialize (H0 (SOAtk pA0 pA' oA ((C atk, c) :: ds) atk0)). cbn in H0. now rewrite Hds in H0.
      (* Opponent defends *)
      + assert (atk1 = atk) as ->.
        { do 2 eapply Eqdep_dec.inj_pair2_eq_dec in H9. assumption. apply option_eq_dec. all: exact dec_f. }
        specialize (H0 (adm o:: pA, psi :: oA, ds) c (SODef (adm o:: pA) oA ds c H11)). cbn in H0.
        now rewrite Hds in H0.
    (* Player defends *)
    - apply (DWS (DPDef pA pC oC H2 H1)). intros s''. inversion 1; subst.
      (* Opponent attacks *)
      + rewrite <- H4 in *. specialize (H0 (pA0 ++ pA', adm0 o:: oA, ds) (C atk0)).
        specialize (H0 (SOAtk pA0 pA' oA ds atk0)). cbn in H0. now rewrite Hds in H0.
      (* Opponent defends *)
      + destruct (split_right Hds) as (ds' & [? ? atk'] & pC' & -> & ->).
        specialize (H0 (psi :: pA, psi0 :: oA, ds') (C atk') (SODef (psi :: pA) oA ds' (C atk') H8)). cbn in H0.
        enough (Heq : split ds' = (oC0, pC')) by now rewrite Heq in H0. cbn in Hds; destruct (split ds'); congruence.
  Qed.

  Lemma svalid_dvalid phi :
    svalid phi -> dvalid _ phi.
  Proof.
    intros []. constructor. assumption. intros. now apply (@swin_dwin ([], A, []) c), H0.
  Qed.
End SGame.

author: uds-psl

repo: fol-completeness-theorems


text:
(**
Exercises on Generalizing the Induction Hypothesis
https://homes.cs.washington.edu/~jrw12/InductionExercises.html
by James Wilcox (2017)
Adapted to SSReflect syntax and Mathcomp library.
*)

From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Fixpoint sum (l : seq nat) : nat :=
  if l is (x :: xs) then x + sum xs
  else 0.

Fixpoint sum_iter' (l : seq nat) (acc : nat) : nat :=
  if l is (x :: xs) then sum_iter' xs (x + acc)
  else acc.

Definition sum_iter (l : seq nat) : nat :=
  sum_iter' l 0.

Lemma sum_iter'_correct l x0 :
  sum_iter' l x0 = x0 + sum l.
Proof.
Admitted.

Theorem sum_iter_correct l :
  sum_iter l = sum l.
Proof.
Admitted.

(** Continuation-passing style
    https://en.wikipedia.org/wiki/Continuation-passing_style
 *)
Fixpoint sum_cont' {A} (l : seq nat) (k : nat -> A) : A :=
  if l is (x :: xs) then sum_cont' xs (fun ans => k (x + ans))
  else k 0.

Definition sum_cont (l : seq nat) : nat :=
  sum_cont' l (fun x => x).

Lemma sum_cont'_correct A l (k : nat -> A) :
  sum_cont' l k = k (sum l).
Proof.
Admitted.

Theorem sum_cont_correct l :
  sum_cont l = sum l.
Proof.
Admitted.

Fixpoint rev_rec {A : Type} (xs : seq A) : seq A :=
  if xs is (x::xs') then
    rev_rec xs' ++ [:: x]
  else xs.

Lemma rev_correct A (l1 l2 : seq A) :
  catrev l1 l2 = rev_rec l1 ++ l2.
Proof.
Admitted.

Theorem rev_iter_correct A (l : seq A) :
  rev l = rev_rec l.
Proof.
Admitted.

Fixpoint map_iter' {A B}
    (f : A -> B) (l : seq A) (acc : seq B) : seq B :=
  if l is (x :: l') then map_iter' f l' (f x :: acc)
  else rev acc.

Definition map_iter {A B} (f : A -> B) l := map_iter' f l [::].

Lemma map_iter'_correct A B (f : A -> B) l1 l2 :
  map_iter' f l1 l2 = rev l2 ++ (map f l1).
Proof.
Admitted.

Theorem map_iter_correct A B (f : A -> B) l :
  map_iter f l = map f l.
Proof.
Admitted.

Inductive expr : Type :=
| Const of nat
| Plus of expr & expr.

Fixpoint eval_expr (e : expr) : nat :=
  match e with
  | Const n => n
  | Plus e1 e2 => eval_expr e1 + eval_expr e2
  end.

Fixpoint eval_expr_iter' (e : expr) (acc : nat) : nat :=
  match e with
  | Const n => n + acc
  | Plus e1 e2 => eval_expr_iter' e2 (eval_expr_iter' e1 acc)
  end.

Definition eval_expr_iter e := eval_expr_iter' e 0.

Lemma eval_expr_iter'_correct e acc :
  eval_expr_iter' e acc = acc + eval_expr e.
Proof.
Admitted.

Theorem eval_expr_iter_correct e :
  eval_expr_iter e = eval_expr e.
Proof.
Admitted.

Fixpoint eval_expr_cont' {A} (e : expr) (k : nat -> A) : A :=
  match e with
  | Const n => k n
  | Plus e1 e2 => eval_expr_cont' e2 (fun n2 =>
                  eval_expr_cont' e1 (fun n1 => k (n1 + n2)))
  end.

Definition eval_expr_cont (e : expr) : nat :=
  eval_expr_cont' e (fun n => n).

Lemma eval_expr_cont'_correct A e (k : nat -> A) :
  eval_expr_cont' e k = k (eval_expr e).
Proof.
Admitted.

Theorem eval_expr_cont_correct e :
  eval_expr_cont e = eval_expr e.
Proof.
Admitted.

Inductive instr := Push (n : nat) | Add.

Definition prog := seq instr.

Definition stack := seq nat.

Fixpoint run (p : prog) (s : stack) : stack :=
  if p is (i :: p') then
    let s' :=
        match i with
        | Push n => n :: s
        | Add => if s is (a1 :: a2 :: s') then a2 + a1 :: s'
                 else s
        end
    in
    run p' s'
  else s.

Fixpoint compile (e : expr) : prog :=
  match e with
  | Const n => [:: Push n]
  | Plus e1 e2 => compile e1 ++ compile e2 ++ [:: Add]
  end.

Lemma run_append p1 p2 s :
  run (p1 ++ p2) s = run p2 (run p1 s).
Proof.
Admitted.

Lemma compile_correct_generalized e s :
  run (compile e) s = (eval_expr e) :: s.
Proof.
Admitted.

Theorem compile_correct e :
  run (compile e) [:: ] = [:: eval_expr e].
Proof.
Admitted.

author: kudryashovaia

repo: coq

save_path: github-repos/coq/kudryashovaia-coq


text:
Require Import A1_Plan A2_Orientation A4_Droite A7_Tactics .
Require Import E2_NotEquidirectedIntersection .
Require Import L6_Tactics .
Require Import M1_SuperImposedLines M2_ParallelLines.

Section SECANT_LINES.

Lemma TwoPointsSecantLine : forall d1 d2 : Line, forall A B : Point,
	OnLine d1 A ->
	OnLine d2 A ->
	OnLine d1 B ->
	~OnLine d2 B ->
	SecantLines d1 d2.
Proof.
	intros.
	assert (A <> B).
	 apply (OnLineDistinct A B d2); immediate11.
	 contrapose0 H2.
	   assert (EqLine d1 d2).
	  apply (ParallelEqLine A); immediate11.
	  apply (EqLineOnLine d1); immediate11.
Qed.

Lemma EqSecantSecantLines : forall d1 d2 d3 : Line,
	EqLine d1 d2 ->
	SecantLines d1 d3 ->
	SecantLines d2 d3.
Proof.
	intros.
	contrapose0 H0.
	apply ParallelLinesSym; apply (ParallelEqParallelLine d3 d2 d1).
	 apply ParallelLinesSym; immediate11.
	 apply EqLineSym; immediate11.
Qed.

Lemma EqEqSecantSecantLines : forall d1 d2 d3 d4 : Line,
	EqLine d1 d2 ->
	EqLine d3 d4 ->
	SecantLines d1 d3 ->
	SecantLines d2 d4.
Proof.
	intros.
	contrapose0 H1.
	apply (EqEqParallelLine d2 d4).
	 apply EqLineSym; immediate11.
	 apply EqLineSym; immediate11.
	 immediate11.
Qed.

Lemma EqNotSecantLines : forall d1 d2: Line,
	EqLine d1 d2 ->
	~SecantLines d1 d2.
Proof.
	intros.
	intro H0; elim H0.
	apply EqParallelLine; immediate11.
Qed.

Lemma SecantNotEqLines : forall d1 d2: Line,
	SecantLines d1 d2 ->
	~EqLine d1 d2.
Proof.
	intros.
	contrapose0 H.
	apply EqParallelLine; immediate11.
Qed.

Lemma FourPointsSecantLines : forall d1 d2 : Line, forall A B C D: Point,
	OnLine d1 A -> OnLine d1 B ->
	OnLine d2 C -> OnLine d2 D ->
	Clockwise A B C ->
	~Clockwise A B D ->
	SecantLines d1 d2.
Proof.
	intros; intro.
	elim (FourPointsSecantLine A B C D H3 H4).
	setLine0 A B ipattern:(d3).
	 immediate11.
	 assert (EqLine d1 d3).
	  apply EqLineDef; immediate11.
	  setLine0 C D ipattern:(d4).
	   step11 H3.
	   assert (EqLine d2 d4).
	    apply EqLineDef; immediate11.
	    assert (ParallelLines d3 d4).
	     apply (EqEqParallelLine d1 d2); immediate11.
	     exact H10.
Qed.

End SECANT_LINES.

author: coq-contribs

repo: euclidean-geometry


text:
(*
(C) Copyright 2010, COQTAIL team

Project Info: http://sourceforge.net/projects/coqtail/

This library is free software; you can redistribute it and/or modify it
under the terms of the GNU Lesser General Public License as published by
the Free Software Foundation; either version 2.1 of the License, or
(at your option) any later version.

This library is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
or FITNESS FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public
License for more details.

You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301,
USA.
*)

Require Export Reals.
Require Import Rsequence.
Require Export MyReals.
Require Import Max.
Require Import Fourier.
Require Import Rsequence_base_facts.

Open Local Scope R_scope.

(** * Definitions *)

(** General term of a Power Serie and its absolute value *)
Definition gt_Pser (An : nat -> R) (x : R) := fun (n:nat) => (An n) * (x ^ n).

Definition gt_abs_Pser (An : nat -> R) (x : R) := fun (n:nat) => Rabs(An n * x ^ n).

Definition An_deriv (An:nat -> R) := fun n => INR (S n) * An (S n).

Definition gt_deriv_Pser (An : nat -> R) (x : R) := gt_Pser (An_deriv An) x.

Definition Pser_abs (An : nat -> R) (x l: R) :=
    Pser (fun n : nat => Rabs (An n)) (Rabs x) l.

(** Lower bound on the cv radius *)

Definition Cv_radius_weak (An : nat -> R) (r:R) := has_ub (gt_abs_Pser An r).

(** Cv radius definition *)

Definition finite_cv_radius (An : nat -> R) (r:R) :=
    (forall r', 0 <= r' < r -> Cv_radius_weak An r') /\
    (forall r', r < r' -> ~ (Cv_radius_weak An r')).

Definition infinite_cv_radius (An : nat -> R) := forall (r : R), Cv_radius_weak An r.

(** * Some lemmas manipulating the definitions *)

Lemma Cv_radius_weak_0 An : Cv_radius_weak An 0.
Proof.
intro An.
exists (Rabs(An O)).
intros x Hx.
destruct Hx as [n Hn].
rewrite Hn.
unfold gt_abs_Pser.
destruct n.
 rewrite pow_O.
  ring_simplify(An 0%nat * 1); apply Rle_refl.

 rewrite pow_i.
 ring_simplify(An(S n)%nat * 0).
 rewrite Rabs_R0; apply Rabs_pos.
omega.
Qed.

Lemma finite_cv_radius_pos An r : finite_cv_radius An r -> 0 <= r.
Proof.
intros An r [_ Hf].
 destruct(Rle_lt_dec 0 r).
  trivial.
destruct (Hf 0).
trivial.
apply Cv_radius_weak_0.
Qed.

Lemma Cv_radius_weak_Rabs_compat : forall (An : nat -> R) (r : R),
       Cv_radius_weak An r -> Cv_radius_weak (fun n => Rabs (An n)) r.
Proof.
intros An r Rho.
elim Rho ; intros m Hm ; exists m ; unfold gt_abs_Pser ; intros a Ha ;
 unfold EUn in Ha ; elim Ha ; intros i Hi ; rewrite Hi ; rewrite Rabs_mult ;
 rewrite Rabs_Rabsolu ; rewrite <- Rabs_mult ; apply Hm ; exists i ; unfold gt_abs_Pser ;
 reflexivity.
Qed.

Lemma pow_lt_compat : forall x y, 0 < x -> x < y ->
  forall n, (1 <= n)%nat -> x ^ n < y ^ n.
Proof.
intros x y x_pos x_lt_y n n_lb.
 induction n.
 apply False_ind ; intuition.
 destruct n.
 simpl ; repeat (rewrite Rmult_1_r) ; assumption.
 assert (Hrew : forall a n, a ^ S (S n) = a * a ^ S n).
  intros a m ; simpl ; reflexivity.
 repeat (rewrite Hrew) ; apply Rmult_gt_0_lt_compat ; [apply pow_lt | | | apply IHn] ; intuition.
 apply Rlt_trans with x ; assumption.
Qed.

Lemma pow_le_compat : forall x y, 0 <= x -> x <= y ->
  forall n, x ^ n <= y ^ n.
Proof.
intros x y x_pos x_lt_y n.
 induction n.
 simpl ; apply Req_le ; reflexivity.
 simpl ; apply Rmult_le_compat ; [| apply pow_le | |] ; assumption.
Qed.

Lemma Cv_radius_weak_le_compat : forall (An : nat -> R) (r r' : R),
       Rabs r' <= Rabs r -> Cv_radius_weak An r -> Cv_radius_weak An r'.
Proof.
intros An r r' r'_bd Rho.
 case (Req_or_neq r') ; intro r_eq.
  rewrite r_eq ; exists (Rabs (An 0%nat)) ; intros x Hx ; destruct Hx as (i, Hi) ;
  rewrite Hi ; unfold gt_abs_Pser ; clear ; induction i ; [apply Req_le ;
  apply Rabs_eq_compat ; field | rewrite pow_i ; intuition ; rewrite Rmult_0_r ;
  rewrite Rabs_R0 ; apply Rabs_pos].
  assert (r_pos : 0 < Rabs r).
   apply Rlt_le_trans with (Rabs r') ; [apply Rabs_pos_lt |] ; assumption.
  assert (r_neq : r <> 0).
   case (Req_or_neq r) ; intro s ; [| assumption] ;
  apply False_ind ; rewrite s in r_pos ; rewrite Rabs_R0 in r_pos ; fourier.
  destruct Rho as (C, HC) ; exists C ; intros x Hx ; destruct Hx as (i,Hi) ; rewrite Hi ;
  unfold gt_abs_Pser.
  replace (r' ^ i) with ((r' ^ i * /r ^ i) * (r ^ i)).
  repeat (rewrite Rabs_mult) ; rewrite Rmult_comm ; rewrite <- Rabs_mult at 1 ;
  rewrite Rmult_assoc ; rewrite <- Rabs_mult.
  apply Rle_trans with (1 * Rabs (r ^ i * An i)).
  apply Rmult_le_compat_r ; [apply Rabs_pos | rewrite Rinv_pow] ;
  [|assumption].
  rewrite <- Rpow_mult_distr ; rewrite <- RPow_abs ; replace 1 with (1 ^ i) ;
  [|apply pow1] ; apply pow_le_compat ; [apply Rabs_pos | rewrite Rabs_mult].
  replace 1 with ((Rabs r) * /(Rabs r)) ; [rewrite Rabs_Rinv ; [apply Rmult_le_compat_r ;
  [apply Rlt_le ; apply Rinv_0_lt_compat |] |] | apply Rinv_r ; apply Rgt_not_eq] ;
  assumption.
  rewrite Rmult_1_l ; rewrite Rmult_comm ; apply HC ; exists i ; reflexivity.
  field ; apply pow_nonzero ; assumption.
Qed.

Lemma finite_cv_radius_weakening : forall An r, finite_cv_radius An r ->
      forall x, Rabs x < r -> Cv_radius_weak An x.
Proof.
intros An r [H_sup _] x Hx.
 apply Cv_radius_weak_le_compat with (Rabs x).
  rewrite Rabs_Rabsolu ; right ; reflexivity.
  apply H_sup ; split ; [apply Rabs_pos | assumption].
Qed.

Lemma Cv_radius_weak_padding_pos_compat : forall (An : nat -> R) (r : R),
     Cv_radius_weak An r -> forall N, Cv_radius_weak (fun n => An (n + N)%nat) r.
Proof.
intros An r Rho N.
 destruct (Req_dec r 0) as [r_eq | r_neq].
  rewrite r_eq ; exists (Rabs (An N)).
  intros u Hu ; destruct Hu as [n Hn] ; rewrite Hn ; unfold gt_abs_Pser ; destruct n.
  simpl ; rewrite Rmult_1_r ; right ; reflexivity.
  rewrite Rabs_mult, pow_i,
  Rabs_R0, Rmult_0_r ; [apply Rabs_pos | intuition].
 destruct Rho as [M HM].
 exists (M * (/ Rabs r) ^ N)%R.
 intros u Hu ; destruct Hu as [n Hn] ; rewrite Hn.
 unfold gt_abs_Pser ; simpl.
 rewrite Rabs_mult ; apply Rle_trans with (Rabs (An (n + N)%nat) * Rabs (r ^ n) *
 (Rabs r ^ N) * ((/Rabs r) ^ N))%R.
 right ; repeat rewrite Rmult_assoc ; repeat apply Rmult_eq_compat_l.
 rewrite <- Rpow_mult_distr, Rinv_r, pow1, Rmult_1_r ; [reflexivity |
 apply Rabs_no_R0 ; assumption].
 apply Rmult_le_compat_r.
 apply pow_le ; left ; apply Rinv_0_lt_compat ; apply Rabs_pos_lt ; assumption.
 rewrite Rmult_assoc, RPow_abs ; apply HM.
 exists (n + N)%nat ; unfold gt_abs_Pser.
 repeat rewrite Rabs_mult ; apply Rmult_eq_compat_l ;
 rewrite <- Rabs_mult ; apply Rabs_eq_compat.
 symmetry ; apply pow_add.
Qed.

Lemma Cv_radius_weak_padding_neg_compat : forall (An : nat -> R) (r : R) (N : nat),
     Cv_radius_weak (fun n => An (n + N)%nat) r -> Cv_radius_weak An r.
Proof.
intros An r N Rho.
 destruct Rho as [M HM].
 destruct (Rseq_partial_bound (fun n => (An n) * r ^ n) N) as [M' HM'].
 destruct (Req_dec r 0) as [r_eq | r_neq].
 exists (Rabs (An 0%nat)) ; intros u Hu ; destruct Hu as [n Hn] ; rewrite Hn.
  unfold gt_abs_Pser ; destruct n.
   simpl ; rewrite Rmult_1_r ; right ; reflexivity.
   rewrite Rabs_mult, r_eq, pow_i, Rabs_R0,  Rmult_0_r ; [apply Rabs_pos | intuition].
 exists (Rmax (M * Rabs (r ^ N)) M') ; intros u Hu ; destruct Hu as [n Hn] ; rewrite Hn.
 destruct (le_lt_dec n N) as [n_lb | n_ub].
 apply Rle_trans with M' ; [apply HM' | apply RmaxLess2] ; assumption.
 apply Rle_trans with (M * Rabs (r ^ N))%R ; [| apply RmaxLess1] ; unfold gt_abs_Pser.
 apply Rle_trans with (Rabs (An n * r ^ n) * (/ Rabs (r ^ N)) * Rabs (r ^ N))%R.
 right ; field ; apply Rabs_no_R0.
 apply pow_nonzero ; assumption.
  apply Rmult_le_compat_r ; [apply Rabs_pos |].
  apply HM ; exists (n - N)%nat.
  unfold gt_abs_Pser.
  rewrite <- RPow_abs, Rinv_pow, <- Rabs_Rinv, RPow_abs, <- Rabs_mult,
  <- Rinv_pow.
  assert (Hrew : (n = n - N + N)%nat).
   intuition.
   repeat rewrite Rabs_mult ; rewrite Hrew at 1 ; rewrite Rmult_assoc ;
   apply Rmult_eq_compat_l ; rewrite <- Rabs_mult ; apply Rabs_eq_compat.
   rewrite Hrew at 1 ; rewrite pow_add, Rmult_assoc, Rinv_r, Rmult_1_r ;
   [reflexivity | apply pow_nonzero ; assumption].
   assumption.
   assumption.
   apply Rabs_no_R0 ; assumption.
Qed.

Lemma Cv_radius_weak_plus : forall (An Bn : nat -> R) (r1 r2 : R),
       Cv_radius_weak An r1 -> Cv_radius_weak Bn r2 ->
       Cv_radius_weak (fun n => An n + Bn n) (Rmin (Rabs r1) (Rabs r2)).
Proof.
intros An Bn r1 r2 RhoA RhoB.
assert (r''_bd1 : Rabs (Rmin (Rabs r1) (Rabs r2)) <= Rabs r1).
 unfold Rmin ; case (Rle_dec (Rabs r1) (Rabs r2)) ; intro H ;
 rewrite Rabs_Rabsolu ; intuition.
assert (r''_bd2 : Rabs (Rmin (Rabs r1) (Rabs r2)) <= Rabs r2).
 unfold Rmin ; case (Rle_dec (Rabs r1) (Rabs r2)) ; intro H ;
 rewrite Rabs_Rabsolu ; intuition.
assert (Rho'A := Cv_radius_weak_le_compat An _ _ r''_bd1 RhoA).
assert (Rho'B := Cv_radius_weak_le_compat Bn _ _ r''_bd2 RhoB).
 destruct Rho'A as (C, HC) ;
 destruct Rho'B as (C', HC') ;
 exists (C + C').
 intros x Hx ; destruct Hx as (i, Hi) ; rewrite Hi ; unfold gt_abs_Pser.
 rewrite Rmult_plus_distr_r ; apply Rle_trans with (Rabs (An i *  Rmin (Rabs r1)
         (Rabs r2) ^ i) + Rabs (Bn i * Rmin (Rabs r1) (Rabs r2) ^ i)) ; [apply Rabs_triang |].
 apply Rle_trans with (Rabs (An i * Rmin (Rabs r1) (Rabs r2) ^ i) + C') ;
 [apply Rplus_le_compat_l ; apply HC' | apply Rplus_le_compat_r ; apply HC] ;
 exists i ; intuition.
Qed.

Lemma Cv_radius_weak_opp : forall (An : nat -> R) (r : R),
       Cv_radius_weak An r ->
       Cv_radius_weak (fun n => - An n) r.
Proof.
intros An r Rho.
 destruct Rho as (C, HC) ; exists C ; intros x Hx ; destruct Hx as (i,Hi) ; rewrite Hi ;
 unfold gt_abs_Pser ; rewrite Ropp_mult_distr_l_reverse ; rewrite Rabs_Ropp ;
 apply HC ; exists i ; intuition.
Qed.

Lemma Cv_radius_weak_minus : forall (An Bn : nat -> R) (r1 r2 : R),
       Cv_radius_weak An r1 -> Cv_radius_weak Bn r2 ->
       Cv_radius_weak (fun n => An n - Bn n) (Rmin (Rabs r1) (Rabs r2)).
Proof.
intros An Bn r1 r2 RhoA RhoB.
 assert (Rho'B := Cv_radius_weak_opp Bn _ RhoB).
 unfold Rminus ; apply Cv_radius_weak_plus ; assumption.
Qed.

Lemma Rmin_ge_0 : forall x y, 0 <= x -> 0 <= y -> 0 <= Rmin x y.
Proof.
intros x y x_pos y_pos.
 unfold Rmin ; case (Rle_dec x y) ; intro h ; intuition.
Qed.

Lemma Pser_add : forall (An Bn : nat -> R) (x : R) (N : nat),
       sum_f_R0 (gt_Pser (fun n => An n + Bn n) x) N = sum_f_R0 (gt_Pser An x) N + sum_f_R0 (gt_Pser Bn x) N.
Proof.
intros An Bn x N ; induction N.
 compute ; field.
 assert (Hrew : forall a b c d e, c = d + e -> a + b + c = a + d + (b + e)).
  intros ; repeat (rewrite Rplus_assoc) ; apply Rplus_eq_compat_l ;
  replace (d + (b + e)) with (b + (d + e)) by field ; apply Rplus_eq_compat_l ;
  assumption.
 simpl ; rewrite IHN ; apply Hrew.
 unfold gt_Pser ; field.
Qed.

Lemma Pser_minus : forall (An Bn : nat -> R) (x : R) (N : nat),
       sum_f_R0 (gt_Pser (fun n => An n - Bn n) x) N = sum_f_R0 (gt_Pser An x) N - sum_f_R0 (gt_Pser Bn x) N.
Proof.
intros An Bn x N ; induction N.
 compute ; field.
 assert (Hrew : forall a b c d e, c = d - e -> a - b + c = a + d - (b + e)).
  intros ; unfold Rminus ; repeat (rewrite Rplus_assoc) ; apply Rplus_eq_compat_l ;
  replace (d + - (b + e)) with (- b + (d - e)) by field ; apply Rplus_eq_compat_l ;
  assumption.
 simpl ; rewrite IHN ; apply Hrew.
 unfold gt_Pser ; field.
Qed.

(** Pser and Un_cv are linked. See "tech12" for the reciprocal lemma *)

Lemma Pser_Rseqcv_link : forall (An : nat -> R) (x l : R),
       Pser An x l ->
       Rseq_cv (fun N : nat => sum_f_R0 (gt_Pser An x) N) l.
Proof.
intros An x l Hyp.
 unfold gt_Pser.
 apply Hyp.
Qed.

Lemma finite_cv_radius_le An r r' :
  finite_cv_radius An r -> Cv_radius_weak An r' -> r' <= r.
Proof.
intros An r r' [_ Hf] Hr'.
 destruct(Rle_lt_dec r' r).
  trivial.
  apply False_ind; apply (Hf r' r0 Hr').
Qed.

Lemma finite_cv_radius_lub An r :
  finite_cv_radius An r -> is_lub (fun r' => Cv_radius_weak An r') r.
Proof.
intros An r H.
split; intros r' Hr'.
 apply finite_cv_radius_le with An; trivial.

 destruct H as [H1 H2].
 destruct (Rle_lt_dec r r').
  trivial.

  pose ((r+r')/2) as r1.
  assert(r' < r1 < r).
   assert(H : forall a, a = (a+a)/2) by (intro; field).
   split; unfold r1; [rewrite (H r') at 1 | rewrite (H r) at 2];
    apply Rmult_lt_compat_r; auto with *.

destruct H as [H H'].
destruct (Hr' r1).
 apply H1; split.
  apply Rle_trans with r'.
   apply Hr', Cv_radius_weak_0; auto with *.
auto with *.
trivial.

 apply False_ind, (Rlt_irrefl r'), Rlt_trans with r1; trivial.

 apply False_ind, (Rlt_irrefl r').
 rewrite <- H0 in *; trivial.
Qed.

(*
Lemma finite_cv_radius_ex An r0 :
 ~ Cv_radius_weak An r0 -> {r | finite_cv_radius An r}.
Proof.

needs classical *)

author: coqtail

repo: coqtail

save_path: github-repos/coq/coqtail-coqtail


text:
(***************************************************************************
* Safety for Simply Typed Lambda Calculus (CBV) - Adequacy                 *
* Brian Aydemir & Arthur Charguéraud, July 2007, Coq v8.1                  *
***************************************************************************)

Set Implicit Arguments.
Require Import Metatheory.

Require Import
  STLC_Core_Definitions
  STLC_Core_Infrastructure
  STLC_Core_Soundness.

(***************************************************************************)
(** * Definitions with the exists-fresh quantification *)

(** Terms are locally-closed pre-terms *)

Inductive eterm : trm -> Prop :=
  | eterm_var : forall x,
      eterm (trm_fvar x)
  | eterm_abs : forall x t1,
      x \notin fv t1 ->
      eterm (t1 ^ x) ->
      eterm (trm_abs t1)
  | eterm_app : forall t1 t2,
      eterm t1 ->
      eterm t2 ->
      eterm (trm_app t1 t2).

(** Typing relation *)

Reserved Notation "E |== t ~: T" (at level 69).

Inductive etyping : env -> trm -> typ -> Prop :=
  | etyping_var : forall E x T,
      ok E ->
      binds x T E ->
      E |== (trm_fvar x) ~: T
  | etyping_abs : forall x E U T t1,
      x \notin dom E \u fv t1 ->
      (E & x ~ U) |== (t1 ^ x) ~: T ->
      E |== (trm_abs t1) ~: (typ_arrow U T)
  | etyping_app : forall S T E t1 t2,
      E |== t1 ~: (typ_arrow S T) ->
      E |== t2 ~: S ->
      E |== (trm_app t1 t2) ~: T

where "E |== t ~: T" := (etyping E t T).

(** Definition of values (only abstractions are values) *)

Inductive evalue : trm -> Prop :=
  | evalue_abs : forall t1,
      eterm (trm_abs t1) -> evalue (trm_abs t1).

(** Reduction relation - one step in call-by-value *)

Inductive ered : trm -> trm -> Prop :=
  | ered_beta : forall t1 t2,
      eterm (trm_abs t1) ->
      evalue t2 ->
      ered (trm_app (trm_abs t1) t2) (t1 ^^ t2)
  | ered_app_1 : forall t1 t1' t2,
      eterm t2 ->
      ered t1 t1' ->
      ered (trm_app t1 t2) (trm_app t1' t2)
  | ered_app_2 : forall t1 t2 t2',
      evalue t1 ->
      ered t2 t2' ->
      ered (trm_app t1 t2) (trm_app t1 t2').

Notation "t -->> t'" := (ered t t') (at level 68).

(** Goal is to prove preservation and progress *)

Definition epreservation := forall E t t' T,
  E |== t ~: T ->
  t -->> t' ->
  E |== t' ~: T.

Definition eprogress := forall t T,
  empty |== t ~: T ->
     evalue t
  \/ exists t', t -->> t'.

(***************************************************************************)
(** * Detailed Proofs of Renaming Lemmas (without high automation)  *)

(* ********************************************************************** *)
(** ** Proving the renaming lemma for [term]. *)

Lemma term_rename : forall x y t,
  x \notin fv t -> term (t ^ x) ->
  y \notin fv t -> term (t ^ y).
Proof.
  introv Frx Wx Fry.
  (* introduce a renaming *)
  rewrite (@subst_intro x).
  (* apply substitution result *)
  apply* subst_term.
  (* use the fact that x is fresh *)
  assumption.
  (* prove term (trm_fvar y) *)
  apply* term_var.
Qed.

(* ********************************************************************** *)
(** ** Proving the renaming lemma for [typing]. *)

Lemma typing_rename : forall x y E t U T,
  x \notin dom E \u fv t -> (E & x ~ U) |= (t ^ x) ~: T ->
  y \notin dom E \u fv t -> (E & y ~ U) |= (t ^ y) ~: T.
Proof.
  introv Frx Typx Fry.
  (* ensure x <> y, so as to be able to build (E & y ~ U & x ~ U) *)
  destruct (x == y). subst*.
  (* assert that E is ok *)
  poses K (proj1 (typing_regular Typx)). inversions K.
  (* introduce substitution *)
  rewrite~ (@subst_intro x).
  (* apply substitution lemma *)
  apply_empty* typing_subst.
  (* apply weakening lemma *)
  poses P (@typing_weaken (x ~ U) E (y ~ U)).
   simpls. apply* P; env_fix.
  (* prove ok (E & y ~ U & x ~ U) *)
  apply* ok_push.
  (* prove (E & y ~ U |= trm_fvar y ~: U) *)
  apply* typing_var.
Qed.

(***************************************************************************)
(** * Proofs of equivalence.  *)

(* ********************************************************************** *)
(** ** Proving the equivalence of [term] and [eterm] *)

Hint Constructors term eterm.

Lemma term_to_eterm : forall t,
  term t -> eterm t.
Proof.
  induction 1; eauto.
  pick_fresh x. apply* (@eterm_abs x).
Qed.

Lemma eterm_to_term : forall t,
  eterm t -> term t.
Proof.
  induction 1; eauto.
  apply_fresh* term_abs as y. apply* term_rename.
Qed.

(* ********************************************************************** *)
(** ** Proving the equivalence of [value] and [evalue] *)

Hint Constructors value evalue.

Lemma value_to_evalue : forall t,
  value t -> evalue t.
Proof.
  induction 1; use term_to_eterm.
Qed.

Lemma evalue_to_value : forall t,
  evalue t -> value t.
Proof.
  induction 1; use eterm_to_term.
Qed.

(* ********************************************************************** *)
(** ** Proving the equivalence of [red] and [ered] *)

Hint Constructors red ered.

Lemma red_to_ered : forall t t',
  red t t' -> ered t t'.
Proof.
  induction 1; use term_to_eterm value_to_evalue.
Qed.

Lemma ered_to_red : forall t t',
  ered t t' -> red t t'.
Proof.
  induction 1; use eterm_to_term evalue_to_value.
Qed.

(* ********************************************************************** *)
(** ** Proving the equivalence of [typing] and [etyping] *)

Hint Constructors typing etyping.

Lemma typing_to_etyping : forall E t T,
  E |= t ~: T  ->  E |== t ~: T.
Proof.
  induction 1; eauto.
  pick_fresh x. apply* (@etyping_abs x).
Qed.

Lemma etyping_to_typing : forall E t T,
  E |== t ~: T  ->  E |= t ~: T.
Proof.
  induction 1; eauto.
  apply_fresh* typing_abs as y. apply* typing_rename.
Qed.

(* ********************************************************************** *)

author: spl


text:
(* Only P1 P2 Preservation and Sound are written by me *)

Inductive Exp : Type :=
  | litN : nat  -> Exp
  | litB : bool -> Exp
  | add  : Exp -> Exp -> Exp
  | cond : Exp -> Exp -> Exp -> Exp.

(* Types *)
Inductive T : Type :=
  | t_nat  : T
  | t_bool : T.

(* Operational semantics, one-step relation *)
Inductive Step : Exp -> Exp -> Prop :=

  | r_add : forall {n1 n2 n3},
      n3 = n1 + n2 -> Step (add (litN n1) (litN n2)) (litN n3)

  | r_cond_true : forall {e1 e2},
      Step (cond (litB true) e1 e2) e1

  | r_cond_false : forall {e1 e2},
      Step (cond (litB false) e1 e2) e2

  | c_add_l : forall {e1 e1' e2},
      Step e1 e1' -> Step (add e1 e2) (add e1' e2)

  | c_add_r : forall {e1 e2 e2'},
      Step e2 e2' -> Step (add e1 e2) (add e1 e2')

  | c_cond : forall {e1 e1' e2 e3},
      Step e1 e1' -> Step (cond e1 e2 e3) (cond e1' e2 e3).

(* Reflexive, transitive closure of Step *)
Inductive Sem : Exp -> Exp -> Prop :=

  | s_refl : forall {e},
      Sem e e

  | s_trans : forall {e1} e2 {e3},
      Step e1 e2 -> Sem e2 e3 -> Sem e1 e3.

(* Example expression *)
Definition ex1 :=
  add (cond (cond (litB false)
                  (litB false) (litB true))
            (litN 2) (litN 3))
      (litN 4).

(* Example semantic derivation *)
Fact s_ex1 : Sem ex1 (litN 6).
Proof.
  unfold ex1.
  apply s_trans with (e2 := add (cond (litB true) (litN 2) (litN 3)) (litN 4)).
    apply c_add_l. apply c_cond. apply r_cond_false.
  apply s_trans with (e2 := add (litN 2) (litN 4)).
    apply c_add_l. apply r_cond_true.
  apply s_trans with (e2 := litN 6).
    apply r_add. compute. reflexivity.
  apply s_refl.
Qed.

(* Typing relation *)
Inductive HasT : Exp -> T -> Prop :=

  | t_litN : forall {n},
      HasT (litN n) t_nat

  | t_litB : forall {b},
      HasT (litB b) t_bool

  | t_add  : forall {e1 e2},
      HasT e1 t_nat -> HasT e2 t_nat -> HasT (add e1 e2) t_nat

  | t_cond : forall {e1 e2 e3 t},
      HasT e1 t_bool -> HasT e2 t -> HasT e3 t -> HasT (cond e1 e2 e3) t.

(* Example typing derivation *)
Fact t_ex1 : HasT ex1 t_nat.
Proof.
  unfold ex1.
  apply t_add.
  apply t_cond.
  apply t_cond.
  apply t_litB. apply t_litB. apply t_litB.
  apply t_litN. apply t_litN. apply t_litN.
Qed.

(* Predicate indicating whether an expression is a value
   of the corresponding type *)
Inductive Value : Exp -> T -> Prop :=
  | v_litN : forall {n}, Value (litN n) t_nat
  | v_litB : forall {b}, Value (litB b) t_bool.

(* Progress: a well-typed term is not stuck *)
Lemma Progress : forall e t,
  HasT e t -> Value e t \/ (exists e', Step e e').
Proof.
  intros.
  induction H.

    (* litN *)
    left. exact v_litN.

    (* litB *)
    left. exact v_litB.

    (* add *)
    right. inversion IHHasT1.
      inversion IHHasT2.
        inversion H1; inversion H2.
          exists (litN (n+n0)).
          apply r_add. reflexivity.
        destruct H2.
          exists (add e1 x).
          apply c_add_r. apply H2.
        destruct H1.
          exists (add x e2).
          apply c_add_l. apply H1.

    (* cond *)
    right. inversion IHHasT1.
      inversion H2.
        destruct b.
          exists e2. apply r_cond_true.
          exists e3. apply r_cond_false.
        destruct H2.
          exists (cond x e2 e3).
            apply c_cond. apply H2.

Qed. (* Whew! *)

Ltac inv_auto H := inversion H; auto.

Lemma P1 : forall e1 e2,
  HasT e1 t_bool -> Step e1 e2 -> HasT e2 t_bool.
Proof.
  intros.
  induction H0; [inv_auto H | inv_auto H | inv_auto H | inv_auto H | inv_auto H | idtac].
  apply t_cond; [apply IHStep; inv_auto H | inv_auto H | inv_auto H].
Qed.

Lemma P2 : forall e1 e2,
  HasT e1 t_nat -> Step e1 e2 -> HasT e2 t_nat.
Proof.
  intros.
  induction H0;
  [apply t_litN | inv_auto H | inv_auto H | apply t_add; inv_auto H | apply t_add; inv_auto H | idtac].
  apply t_cond; [apply P1 with (e1 := e1); inv_auto H | inv_auto H | inv_auto H].
Qed.

(* Preservation: if a term is well-typed before a step,
   then it is well-typed after a step. *)
Lemma Preservation : forall e1 e2 t1,
  HasT e1 t1 -> Step e1 e2 -> (exists t2, HasT e2 t2).
Proof.
  intros.
  exists t1.
  destruct t1.
  apply P2 with (e1 := e1); auto.
  apply P1 with (e1 := e1); auto.
Qed.

(* Soundness: the type system is sound if it ensures progress
   and preservation. *)
Theorem Sound : forall e e' t,
  HasT e t -> (Value e t \/ (exists e', Step e e'))
           /\ (Step e e' -> (exists t', HasT e' t')).
Proof.
  intros.
  split.
  apply Progress.
  exact H.
  intros.
  apply Preservation with (e1 := e) (t1 := t); auto.
Qed.

author: FiveEyes

repo: playground

save_path: github-repos/coq/FiveEyes-playground


text:
Require Import Coqlib Integers Floats Errors Globalenvs.
Require Import AST Linking Values Memory Csyntax Clight.

Inductive set_destination : Type :=
  | SDbase (tycast ty: type) (tmp: AST.ident)
  | SDcons (tycast ty: type) (tmp: AST.ident) (sd: set_destination).

Inductive destination : Type :=
  | For_val
  | For_effects
  | For_set (sd: set_destination).

Fixpoint do_set (sd: set_destination) (a: expr) : list statement :=
  match sd with
  | SDbase tycast ty tmp => Sset tmp (Ecast a tycast) :: nil
  | SDcons tycast ty tmp sd' => Sset tmp (Ecast a tycast) :: do_set sd' (Etempvar tmp ty)
  end.

Definition finish (dst: destination) (sl: list statement) (a: expr) :=
  match dst with
  | For_val => (sl, a)
  | For_effects => (sl, a)
  | For_set sd => (sl ++ do_set sd a, a)
  end.

Definition sd_temp (sd: set_destination) :=
  match sd with SDbase _ _ tmp => tmp | SDcons _ _ tmp _ => tmp end.
Definition sd_seqbool_val (tmp: AST.ident) (ty: type) :=
  SDbase type_bool ty tmp.
Definition sd_seqbool_set (ty: type) (sd: set_destination) :=
  let tmp :=  sd_temp sd in SDcons type_bool ty tmp sd.

Fixpoint eval_simpl_expr (a: expr) : option val :=
  match a with
  | Econst_int n _ => Some(Vint n)
  | Econst_float n _ => Some(Vfloat n)
  | Econst_single n _ => Some(Vsingle n)
  | Econst_long n _ => Some(Vlong n)
  | Ecast b ty =>
      match eval_simpl_expr b with
      | None => None
      | Some v => sem_cast v (typeof b) ty Mem.empty
      end
  | _ => None
  end.

Function makeif (a: expr) (s1 s2: statement) : statement :=
  match eval_simpl_expr a with
  | Some v =>
      match bool_val v (typeof a) Mem.empty with
      | Some b => if b then s1 else s2
      | None   => Sifthenelse a s1 s2
      end
  | None => Sifthenelse a s1 s2
  end.

Fixpoint makeseq_rec (s: statement) (l: list statement) : statement :=
  match l with
  | nil => s
  | s' :: l' => makeseq_rec (Ssequence s s') l'
  end.

Definition makeseq (l: list statement) : statement := makeseq_rec Sskip l.

Definition dummy_expr := Econst_int Int.zero type_int32s.

Definition final (dst: destination) (a: expr) : list statement :=
  match dst with
  | For_val => nil
  | For_effects => nil
  | For_set sd => do_set sd a
  end.

author: Artalik

repo: monad-frame-src


text:
(****************************************************************************)
(* Copyright 2021 The Project Oak Authors                                   *)
(*                                                                          *)
(* 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.                                           *)
(****************************************************************************)

Require Import Coq.micromega.Lia.

Require Import Cava.Cava.
Require Import Cava.Lib.Decoder.

Require Import Cava.Lib.Lib.
Require Import Cava.Lib.CombinationalProperties.
Require Import Cava.Lib.CombinatorsProperties.
Require Import Cava.Lib.MultiplexersProperties.
Require Import Cava.Lib.CavaPreludeProperties.
Require Import Cava.Lib.VecProperties.

Require Import Cava.Util.Bool.
Require Import Cava.Util.List.
Require Import Cava.Util.Nat.
Require Import Cava.Util.Vector.
Require Import Cava.Util.BitArithmeticProperties.
Require Import Cava.Util.Tactics.
Require Import Cava.Semantics.Combinational.

Existing Instance CombinationalSemantics.

Import Circuit.Notations.

Lemma fold_mono {A B n} {a:A} {b: A-> B} {f unit decider}
  (dec_true : forall c d, decider c d = true <-> c = d)
  (right_id : forall c, f c unit = c)
  (neutral : forall c, f c c = c)
  (vec : Vector.t A n) :
  Vector.fold_left f (b a) (Vector.map (fun v => if decider a v then b v else unit) vec) = b a.
Proof.
  induction vec; [ trivial | ].
  cbn.
  case_eq (decider a h); intro H.
  { rewrite dec_true in H. subst.
    rewrite neutral.
    apply IHvec. }
  { remember (dec_contrapositive dec_true) as dec_false.
    rewrite dec_false in H. subst.
    rewrite right_id.
    apply IHvec. }
Qed.

Lemma fold_units {A B n} {a:A} {b: A -> B} f unit decider
  (dec_correct : forall c d, decider c d = true <-> c = d)
  (left_id : forall c, f unit c = c)
  (right_id : forall c, f c unit = c)
  (neutral : forall c, f c c = c)
  (vec : Vector.t A n)
  (guard : Vector.InV a vec) :
  Vector.fold_left f unit (Vector.map (fun v => if decider a v then b v else unit) vec) = b a.
Proof.
  induction vec; [ inversion guard | ]. cbn.
  rewrite left_id.
  case_eq (decider a h); intro a_is_h; [ | ].
  { apply dec_correct in a_is_h. destruct a_is_h.
    apply (@fold_mono A B n a b f unit decider dec_correct right_id neutral). }
  { remember (dec_contrapositive dec_correct) as dec_rev_correct.
    rewrite dec_rev_correct in a_is_h.
    apply IHvec.
    inversion guard; [ | ].
    { exfalso. apply a_is_h. assumption. }
    { assumption. }
  }
Qed.

Theorem fold_units' : forall A n (a:A) f unit decider,
  (forall c d, decider c d = true <-> c = d) ->
  (forall c, f unit c = c) ->
  (forall c, f c unit = c) ->
  (forall c, f c c = c) ->
  forall (vec : Vector.t A n) vec'
  (eq : vec' = Vector.map (fun v => if decider a v then a else unit) vec),
  Vector.InV a vec ->
  Vector.fold_left f unit vec' = a.
Proof. intros. rewrite eq. apply @fold_units with (b:= fun x => a); assumption. Qed.

Theorem enc_dev_inv (n:nat) input : simulate ((Comb (decoder (n:=n))) >==>
  (Comb (encoder (n:=n)))) input = input.
Proof.
  (* Rewrite to [encoder ( decoder ) = id] *)
  autorewrite with push_simulate.
  rewrite map_map.
  apply List.map_id_ext.
  clear input. intros.

  cbv [decoder encoder]. simpl_ident.
  repeat rewrite Vector.map_map.
  rewrite map2_map.
  rewrite map2_drop_same.
  rewrite @tree_equiv with (t:=Vec Bit n) (id:=Vector.const false n); [ | | | | ].
  (* Main branch *)
  { cbv in a.
    rewrite Vector.map_ext with
      (g := fun k =>
              if combType_eqb (t:=Vec Bit n) (N2Bv_sized n (N.of_nat k)) a
                 then N2Bv_sized n (N.of_nat k)
                 else Vector.const false n).
    2 :{ intros a0. simpl_ident.
         replace (N2Bv_sized n (N.of_nat a0)) with
                 (fst ((N2Bv_sized n (N.of_nat a0)),a)); trivial.
         rewrite <- @eqb_correct with (t:=Vec Bit n). simpl.
         rewrite map2_correct. rewrite map2_correct. rewrite map2_swap. cbn.
         unfold xnorb.
         replace ((Vector.map2 (fun b a1 : bool => negb (xorb a1 b))
                               (N2Bv_sized n (N.of_nat a0)) a)) with
                 ((Vector.map2 (fun a1 b : bool => negb (xorb a1 b))
                               (N2Bv_sized n (N.of_nat a0)) a)) ; [ trivial | ].
         apply map2_ext.
         intros. rewrite xorb_comm. trivial. }
    rewrite fold_left_ext with
      (g := fun a b : Vector.t bool n =>
              Vector.map2 (fun x y => x || y) a b).
    2 :{ intros. simpl_ident.
         apply map2_ext. trivial. }
    replace (Vector.map
              (fun k : nat =>
                if combType_eqb (t := Vec Bit n) (N2Bv_sized n (N.of_nat k)) a
                  then N2Bv_sized n (N.of_nat k)
                  else Vector.const false n) (vseq 0 (2 ^ n)))
      with
           (Vector.map
             (fun k =>
               if combType_eqb (t:=Vec Bit n) k a
                 then k
                 else Vector.const false n)
             (Vector.map
               (fun k => (N2Bv_sized n (N.of_nat k)))
               (vseq 0 (2 ^ n)))); [ | ].
    2 :{ rewrite Vector.map_map. trivial. }
    apply fold_units' with
      (decider := combType_eqb (t := Vec Bit n))
      (vec := Vector.map
                (fun k => N2Bv_sized n (N.of_nat k))
                (vseq 0 (2 ^ n))) ; [ | | | | | ].
    { apply combType_eqb_true_iff. }
    { induction c; trivial; [].
      cbn.
      rewrite IHc; trivial. }
    { induction c; trivial; [].
      cbn.
      rewrite IHc; trivial; [].
      destruct h; trivial. }
    { induction c; trivial; [].
      cbn.
      rewrite IHc; trivial; [].
      destruct h; trivial. }
    { apply Vector.map_ext.
      intros a0. cbn in a0.
      assert
        (forall a b, combType_eqb (t:=Vec Bit n) a b = false <-> a <> b)
        as combType_eqb_false_iff.
      { intros. apply iffb. apply combType_eqb_true_iff. }
      case_eq (combType_eqb (t:=Vec Bit n) a0 a);
        case_eq (combType_eqb (t:=Vec Bit n) a a0);
        repeat rewrite combType_eqb_true_iff;
        repeat rewrite combType_eqb_false_iff;
        trivial; [ | ].
      { intros neq eq. exfalso. apply neq. easy. }
      { intros eq neq. exfalso. apply neq. easy. }
    }
    { apply Bv_span. }
  }

  (* side conditions *)
  { intros. simpl_ident.
    rewrite map2_const.
    rewrite Vector.map_id. trivial. }
  { intros. simpl_ident.
    rewrite map2_swap.
    rewrite map2_const.
    simpl.
    rewrite Vector.map_ext with (g := id); [ | ].
    { apply Vector.map_id. }
    { intros. apply orb_comm. }
  }
  { intros. simpl_ident.
    apply map2_assoc.
    intros. apply orb_assoc. }
  { clear a. induction n; [ easy | ]. cbn.
    remember (2^n) as x.
    lia. }
Qed.

Definition N2hotv {n} k : Bvector n := Vector.map (fun m => if Nat.eqb k m then one else zero) (vseq 0 n).

Lemma map_id_guard : forall A f (g : A -> Prop) l
  (ext : forall (a : A),  g a -> f a = a)
  (guard : Forall g l),
  map f l = l.
Proof.
  intros.
  induction l.
  { trivial. }
  { simpl. rewrite ext.
    { rewrite IHl; trivial.
      inversion guard. trivial. }
    { inversion guard. trivial. }
  }
Qed.

Theorem map_ext_guard
  (A B : Type) (f g : A -> B)
  (P : A -> Prop)
  (ext : forall a : A, P a ->  f a = g a)
  (n : nat) (v : Vector.t A n)
  (Guard: forall a : A, InV a v -> P a)
  : Vector.map f v = Vector.map g v.
Proof.
  intros.
  induction v; [ trivial | ].
  cbn.
  rewrite IHv.
  { assert (f h = g h) as H.
    { apply ext. apply Guard. compute. left. reflexivity. }
    inversion H.
    reflexivity.
    }
  { intros. apply Guard.
    cbn. right.  assumption. }
Qed.

Lemma N_lt_step a : (N.of_nat a < N.of_nat (S a))%N.
Proof. rewrite Nat2N.inj_succ. apply N.lt_succ_diag_r. Qed.

Lemma N_lt_inj a b : a < b -> (N.of_nat a < N.of_nat b)%N.
Proof.
  rewrite <- N.compare_lt_iff.
  rewrite <- Nat.compare_lt_iff.
  rewrite Nat2N.inj_compare.
  trivial.
Qed.

Theorem dec_enc_inv (n:nat) (k : nat): k < 2^n ->
  @decoder combType Combinational.CombinationalSemantics n (encoder (N2hotv k)) = N2hotv k.
Proof.
  intro guard.
  cbv [decoder encoder].
  simpl_ident.
  autorewrite with vsimpl.
  cbv [combType].
  rewrite @tree_equiv with (t:=Vec Bit (n)) (id := Vector.const false (n));
   [ | | | | ].
  2:{ intros. simpl_ident. clear. induction n.
      { autorewrite with vsimpl. apply Vector.case0. trivial. }
      { rewrite const_cons. rewrite map2_cons. simpl. rewrite IHn.
        rewrite Vector.eta. trivial. }
  }
  2:{ intros. simpl_ident. clear. induction n.
      { autorewrite with vsimpl. apply Vector.case0. trivial. }
      { rewrite const_cons. rewrite map2_cons. simpl. rewrite IHn.
        rewrite orb_false_r.
        rewrite Vector.eta. trivial. }
  }
  2:{ intros. simpl_ident. apply map2_assoc.
      intros. apply orb_assoc. }
  2:{ clear. induction n.
      { easy. }
      { simpl. remember (2^n) as x. lia. }
  }
  { cbv [N2hotv].
    apply map_ext_guard with (P := fun i => i < 2^n );
      [ | intros a H; apply InV_seq in H; lia ].
    intros a.
    cbv [combType].
    rewrite Vector.map_map.
    rewrite map2_map.
    rewrite map2_drop_same.
    erewrite fold_left_ext;
      [ | intros ; simpl_ident; trivial ].
    rewrite Vector.map_ext with
      (f:= fun x =>
        mux2 (if (k =? x)%nat then one else zero)
          (defaultSignal,
           @Vec.bitvec_literal combType _ _ (N2Bv_sized n (N.of_nat x))))
      (g := fun x =>
        (if (k =? x)%nat
         then @Vec.bitvec_literal combType _ _ (N2Bv_sized n (N.of_nat x))
         else Vector.const false n)).
    2:{ intro a0. rewrite mux2_correct.
        case_eq(k=?a0)%nat; trivial. }
    rewrite fold_units; [ | | | | | ].
    { intros H. case_eq (k=?a)%nat.
      { intros H0.
        apply eq_sym in H0. apply EqNat.beq_nat_eq in H0. subst. simpl.
        simpl_ident.
        rewrite Vector.map2_map.
        rewrite map2_drop_same.
        rewrite Vector.map_ext with (g := fun x => true).
        2: { intros. cbv [xnorb]. rewrite xorb_nilpotent. trivial. }
        rewrite map_to_const.
        apply fold_left_andb_true. }
      { intros H0. apply EqNat.beq_nat_false in H0.
        rewrite eqb_correct.
        simpl.
        rewrite Vector.map_id.
        rewrite Vector.map_id.
        assert(
          Vector.eqb bool
            (fun x y : bool => Bool.eqb x y)
            (N2Bv_sized n (N.of_nat k))
            (N2Bv_sized n (N.of_nat a))
          = true
          -> False).
        { intros H1. apply H0. apply Vector.eqb_eq in H1.
          { apply f_equal with (f:=Bv2N) in H1. rewrite Bv2N_N2Bv_sized in H1.
            { rewrite Bv2N_N2Bv_sized in H1.
              { apply Nat2N.inj.  assumption. }
              { assert (N.of_nat 2 = 2%N) as H2; trivial.
                rewrite <- H2.
                rewrite Nat2N.inj_pow.
                apply  N_lt_inj.
                assumption. }
            }
            { assert (N.of_nat 2 = 2%N) as H2; trivial.
              rewrite <- H2.
              rewrite Nat2N.inj_pow.
              apply  N_lt_inj.
              assumption. }
          }
          { intros. split.
            { apply Bool.eqb_prop. }
            { intros. subst. destruct y; auto. }
          }
        }
        { case_eq(Vector.eqb bool
            (fun x y : bool => Bool.eqb x y)
            (N2Bv_sized n (N.of_nat k))
            (N2Bv_sized n (N.of_nat a))).
          { intros. exfalso. auto. }
          { trivial. }
        }
      }
    }
    { intros. split.
      { intros.
        apply EqNat.beq_nat_true.
        assumption. }
      { intros. subst. apply Nat.eqb_refl. }
    }
    { intros. rewrite Vector.map2_const. simpl. apply Vector.map_id. }
    { intros. rewrite Vector.map2_swap. rewrite Vector.map2_const.
      erewrite Vector.map_ext.
      2: { intros. apply orb_comm. }
      {  apply Vector.map_id. }
    }
    { intros. rewrite Vector.map2_drop_same. erewrite Vector.map_ext.
      2:{ intros. apply orb_diag. }
      { apply Vector.map_id. }
    }
    { apply InV_seq. lia. }
  }
Qed.

author: project-oak

repo: silveroak

save_path: github-repos/coq/project-oak-silveroak