text:
(* Full safety for STLC (Coq 8.14) *)

(* copied from nano0.v *)

(* This version prohibits recursion, and we prove that   *)
(* evaluation always terminates with a well-typed value. *)
(* From this follows both type soundness and strong      *)
(* normalization for STLC.                               *)

(* copied from nano0-total.v *)
(* copied from nano0-total-lr.v *)

(* This version enables recursion again, and we use a    *)
(* step-indexed logical relation to show soundness only. *)

(* Note: we need actual step-indexes, not depth fuel !!! *)

Require Import Coq.Lists.List.
Import ListNotations.
Require Import Arith.EqNat.
Require Import Arith.Le.
From Coq Require Import Lia.
Require Import Lia.
Require Import Coq.Arith.Peano_dec.

Module STLC.

Definition id := nat.

Inductive ty : Type :=
  | TBool  : ty
  | TFun   : ty -> ty -> ty
.

Inductive tm : Type :=
  | ttrue : tm
  | tfalse : tm
  | tvar : id -> tm
  | tapp : tm -> tm -> tm (* f(x) *)
  | tabs : tm -> tm (* \f x.y *)
.

Inductive vl : Type :=
| vbool : bool -> vl
| vabs  : list vl -> tm -> vl
.

Definition venv := list vl.
Definition tenv := list ty.

#[local] Hint Unfold venv : core.
#[local] Hint Unfold tenv : core.

Fixpoint length {X: Type} (l : list X): nat :=
  match l with
    | [] => 0
    | _::l' => 1 + length l'
  end.

Fixpoint index {X : Type} (n : id) (l : list X) : option X :=
  match l with
    | [] => None
    | a :: l'  => if eq_nat_dec n (length l') then Some a else index n l'
  end.

Inductive has_type : tenv -> tm -> ty -> Prop :=
| t_true: forall env,
           has_type env ttrue TBool
| t_false: forall env,
           has_type env tfalse TBool
| t_var: forall x env T1,
           index x env = Some T1 ->
           has_type env (tvar x) T1
| t_app: forall env f x T1 T2,
           has_type env f (TFun T1 T2) ->
           has_type env x T1 ->
           has_type env (tapp f x) T2
| t_abs: forall env y T1 T2,
           has_type (T1::(TFun T1 T2)::env) y T2 ->
           has_type env (tabs y) (TFun T1 T2)
.

(*
None             means timeout
Some None        means stuck
Some (Some v))   means result v
*)

(* this step-indexed version returns the number of steps taken (always <= fuel) *)

Fixpoint teval(n: nat)(env: venv)(t: tm){struct n}: (nat * option (option vl)) :=
  match n with
    | 0 => (0,None)
    | S n =>
      match t with
        | ttrue                                => (1, Some (Some (vbool true)))
        | tfalse                               => (1, Some (Some (vbool false)))
        | tvar x                               => (1, Some (index x env))
        | tabs y                               => (1, Some (Some (vabs env y)))
        | tapp ef ex                           =>
          match teval n env ef with
            | (df, None)                       => (1+df, None)
            | (df, Some None)                  => (1+df, Some None)
            | (df, Some (Some (vbool _)))      => (1+df, Some None)
            | (df, Some (Some (vabs env2 ey))) =>
              match teval (n-df) env ex with
                | (dx, None)                   => (1+df+dx, None)
                | (dx, Some None)              => (1+df+dx, Some None)
                | (dx, Some (Some vx))         =>
                  match teval (n-df-dx) (vx::(vabs env2 ey)::env2) ey with
                    | (dy, res)                => (1+df+dx+dy, res)
                  end
              end
          end
      end
end.

(* some facts about evaluation. we need evaluation to be deterministic so that
   we can "downgrade" our logical relation val_type below. instead of proving
   this fact here, it could also be possible to encode it in the LR itself. *)

Lemma eval_deterministic: forall m n, n < m -> forall H t n1 r j,
  teval n H t = (n1, Some r) -> j >= n ->
  teval j H t = (n1, Some r).
Proof.
  intros m. induction m. intros. inversion H.
  intros. destruct n. inversion H1. destruct j. inversion H2.
  destruct t; simpl; simpl in H1; try eauto.
  remember (teval n H0 t1) as tf. destruct tf as [nf [rf|]].
  rewrite IHm with (n:=n) (n1:=nf) (r:=rf).
  destruct rf; try destruct v; try solve [inversion H1; eauto].
  remember (teval (n-nf) H0 t2) as tx. destruct tx as [nx [rx|]].
  rewrite IHm with (n:=n-nf) (n1:=nx) (r:=rx).
  destruct rx; try solve [destruct v; inversion H1; eauto].
  remember (teval (n-nf-nx) (v :: vabs l t :: l) t) as ty. destruct ty as [ny [ry|]].
  rewrite IHm with (n:=n-nf-nx) (n1:=ny) (r:=ry).

  eauto. lia. eauto. lia.
  inversion H1. inversion H1.
  eauto. lia. eauto. lia.
  inversion H1.
  lia. eauto. lia.
  inversion H1.
Qed.

(* original termination and determinism def: *)
(* Definition tevaln env e v := exists nm, forall n, n > nm -> teval n env e = Some (Some v). *)

(* if we want to encode determinism directly, we'd need something like this: *)
Definition tevaln nm env e n1 v :=
  teval nm env e = (nm, None) \/
  forall n, n > nm -> teval n env e = (n1, Some (Some v)).

(* need to use Fixpoint because of positivity restriction *)
Fixpoint val_type n v T {struct n}: Prop := match v, T with
| vbool b, TBool => True
| vabs env y, TFun T1 T2 =>  match n with | 0 => True | S n0 =>
  (* forall n nx, R n nx H tx vx T1 -> R (n-nx) ny (vx::vf::H) vy T2 *)
  (* NOTE: trouble b/c R does not include vx!! *)
  forall nx vx, nx <> 0 ->
      val_type (S n0 - (S(nx-1))) vx T1 -> forall ry ny,
      (* R nm (vx::(vabs env y)::env) y T2 *)
      teval (n-nx) (vx::(vabs env y)::env) y = (ny, Some ry) ->
      exists vy,
        ny <> 0 /\ ry = Some vy /\ val_type (n0-(nx-1)-ny) vy T2
  end
| _,_ => False
end.

(* unfolding lemma is handy, otherwise we need to destruct n.
   we also take the opportunity to rewrite n/nx into saner form *)
Lemma val_type_unfold: forall n v T, val_type n v T <-> match v, T with
| vbool b, TBool => True
| vabs env y, TFun T1 T2 =>  match n with | 0 => True | S n0 =>
  (* forall n nx, R n nx H tx vx T1 -> R (n-nx) ny (vx::vf::H) vy T2 *)
  (* NOTE: trouble b/c R does not include vx!! *)
  forall nx vx, nx <> 0 ->
      val_type (n-nx) vx T1 -> forall ry ny,
      (* R nm (vx::(vabs env y)::env) y T2 *)
      teval (n-nx) (vx::(vabs env y)::env) y = (ny, Some ry) ->
      exists vy,
        ny <> 0 /\ ry = Some vy /\ val_type (n-nx-ny) vy T2
  end
| _,_ => False
end.
Proof.
  intros. destruct n. simpl. split. eauto. eauto.
  simpl. destruct v; destruct T; try solve [split; eauto].
  split.
  - intros. specialize (H nx vx H0). assert (n - (nx - 1) = S n -nx) as R. lia. rewrite R in H. eapply H; eauto.
  - intros. specialize (H nx vx H0). destruct nx. destruct H0. eauto.
    assert ((S nx - 1) = nx) as R. lia. rewrite R. eapply H. rewrite R in H1. eapply H1. eauto.
Qed.

Definition R n H t T :=
  (* tevaln H t v /\ val_type v T. *)
  forall r n1, teval n H t = (n1,Some r) ->
    exists v, n1 <> 0 /\ r = Some v /\ val_type (n-n1) v T.

Definition R_env nm venv tenv :=
  length venv = length tenv /\
  forall x T1, index x tenv = Some T1 ->
    R nm venv (tvar x) T1.

#[local] Hint Constructors ty : core.
#[local] Hint Constructors tm : core.
#[local] Hint Constructors vl : core.

#[local] Hint Constructors has_type : core.
(* Hint Constructors val_type. *)

#[local] Hint Constructors option : core.
#[local] Hint Constructors list : core.

Lemma V_down: forall n j v T, j <= n -> val_type n v T -> val_type j v T.
Proof.
  intros n. induction n.
  intros. destruct j. eauto. inversion H.
  intros.
  case_eq (eq_nat_dec j (S n)); intros E _. subst j. eauto.
  assert (val_type n v T). {
    rewrite val_type_unfold. rewrite val_type_unfold in H0.
    destruct T; destruct v; try eauto.
    destruct n. eauto. intros. eapply (H0 (S nx) vx _ H2 ry ny). eauto.
  }
  eapply IHn. lia. eauto. Unshelve. lia.
Qed.

Lemma R_down: forall n j H t T, j <= n -> R n H t T -> R j H t T.
Proof.
  intros.
  unfold R. unfold R in H1. intros. eapply eval_deterministic in H2.
  specialize (H1 r n1 H2).
  destruct H1 as [v [N [R ?]]].
  eapply V_down in H1. eauto. lia. eauto. lia.
Qed.

Lemma R_env_down: forall n j H G, j <= n -> R_env n H G -> R_env j H G.
Proof.
  intros.
  unfold R_env. unfold R_env in H1. destruct H1.
  split. eauto. intros.
  eapply R_down in H2. eauto. eauto. eauto.
Qed.

(* if well-typed, then result is an actual value (not stuck and not a timeout),
   for large enough n *)

Theorem full_total_safety : forall nn, forall n, n < nn -> forall e tenv T,
  has_type tenv e T -> forall venv, R_env n venv tenv ->
  R n venv e T.

Proof.
  intros nn. induction nn.
  (* z *) intros. solve [inversion H].
  (* S n *)
  intros n NB ? ? ? W.
  destruct n. unfold R. intros. inversion H0.

  inversion W; intros ? WFE.

  - (* Case "True".  *)
    eexists. simpl in H2. inversion H2. repeat split; try rewrite val_type_unfold; eauto.

  - (* Case "False". *)
    eexists. simpl in H2. inversion H2. repeat split; try rewrite val_type_unfold; eauto.

  - (* Case "Var". *)
    eapply WFE. eauto.

  - (* Case "App". *)
    unfold R. intros ? n1 EVY.
    simpl in EVY.

    assert (R n venv0 f (TFun T1 T)) as RF. eapply IHnn. lia. eauto.
    eapply R_env_down. instantiate (1 := S n). lia. eauto.
    unfold R in RF.

    remember (teval n venv0 f) as EF. symmetry in HeqEF.
    destruct EF as [nf [rf|]]; try solve [inversion EVY].
    destruct (RF rf nf) as [vf [? [EQVF VTF]]]. eauto.
    subst rf.

    rewrite val_type_unfold in VTF. destruct vf. contradiction.

    assert (R (n-nf) venv0 x T1) as RX. eapply IHnn. lia. eauto. eauto.
    eapply R_env_down. instantiate (1 := S n). lia. eauto.
    unfold R in RX.

    remember (teval (n-nf) venv0 x) as EX. symmetry in HeqEX.
    destruct EX as [nx [rx|]]; try solve [inversion EVY].
    destruct (RX rx nx) as [vx [? [EQVX VTX]]]. eauto.
    subst rx.

    remember (teval (n - nf - nx) (vx :: vabs l t :: l) t) as EY. symmetry in HeqEY.
    destruct EY as [ny [ry|]]; try solve [inversion EVY].
    inversion EVY. subst r n1. clear EVY.

    remember (n-nf) as nnf. destruct nnf. inversion HeqEX. rewrite Heqnnf in *. clear Heqnnf. (* can't be zero *)

    specialize (VTF _ _ H5 VTX _ _ HeqEY).
    assert ((n - nf - nx - ny = S n - S (nf + nx + ny))) as RW. lia.
    rewrite <-RW.
    destruct VTF as [? [? [? ?]]]. eexists. repeat split; eauto.

  - (* Case "Abs". *)

    (* goal:  R (S n) venv0 (tabs y) (TFun T1 T2) *)
    unfold R. intros ? ? EV.
    inversion EV.
    simpl in EV. inversion EV. subst n1 r. clear EV.
    exists (vabs venv0 y). split. eauto. split. eauto.
    assert (S n - 1 = n). lia. rewrite H3.

    (* goal val_type n (vabs venv0 y) (TFun T1 T2) *)

    (* internal induction *)
    assert (forall nm1, nm1 <= n -> forall nm, nm <= nm1 ->
                       val_type nm (vabs venv0 y) (TFun T1 T2)) as IND.
    intros nm1. induction nm1.
    (* z *) simpl. intros. destruct nm. simpl. eauto. solve [inversion H5].
    (* s n *) intros ? ? ?.

    (* goal val_type n (vabs venv0 y) (TFun T1 T2) *)
    destruct nm; rewrite val_type_unfold. eauto.
    intros ? ? ? ?.

    eapply IHnn. lia. eauto.

    (* now downgrade and extend R_env *)
    (* goal: (R_env (n-nx) (vx :: vabs venv0 y :: venv0) (T1::TFun T1 T2::tenv0)) as WFE1. *)

    unfold R_env. split. simpl. unfold R_env in WFE. destruct WFE as [L IX]. rewrite L. eauto.
      intros ? ? IX.

      unfold R. intros ? ? EVX.
      remember (S nm-nx) as nx2.
      destruct nx2. solve [inversion EVX].
      simpl in EVX. destruct WFE as [L WX].
      simpl in IX. rewrite <-L in IX.
      (* is it the arg? *)
      destruct (eq_nat_dec x (S (length venv0))).
      inversion EVX. subst n1 r.
      exists vx. split. eauto. split. eauto. simpl.
      inversion IX. subst T0.
      eapply V_down. instantiate (1:= S nx2). lia. eauto.
      (* is it the fun? *)
      destruct (eq_nat_dec x (length venv0)).
      inversion EVX. subst n1 r.
      inversion IX. subst T0.
      rewrite Heqnx2.

      exists (vabs venv0 y). split. eauto. split. eauto.
      (* goal:  val_type (n-nx-1) (vabs venv0  y) (TFun T1 T2) *)
      (* induction! *)
      eapply IHnm1. eauto. lia. lia.

      (* default case *)
      eapply R_down. instantiate (1:= S n). lia. eapply WX. eauto. simpl. eauto.

      (* done with indunction *)
      eapply IND. eauto. eauto.
Qed.

End STLC.

author: TiarkRompf

repo: minidot

save_path: github-repos/coq/TiarkRompf-minidot


text:
(*******************************************************************************
*                                                                              *
*   TypeSize.v                                                                 *
*   Xuejing Huang 2021                                                         *
*   Distributed under the terms of the GPL-v3 license                          *
*                                                                              *
*   This file is part of DistributingTypes.                                    *
*                                                                              *
*   DistributingTypes is free software: you can redistribute it and/or modify  *
*   it under the terms of the GNU General Public License as published by       *
*   the Free Software Foundation, either version 3 of the License, or          *
*   (at your option) any later version.                                        *
*                                                                              *
*   DistributingTypes 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 General Public License for more details.                               *
*                                                                              *
*   You should have received a copy of the GNU General Public License          *
*   along with DistributingTypes.  If not, see <https://www.gnu.org/licenses/>.*
*                                                                              *
*******************************************************************************)

(* This file defines size on types and proves some related
lemmas. It aims to make later proofs easier if they do
induction on the size of types *)

Require Import LibTactics.
Require Export Coq.micromega.Lia.
Require Export Definitions.

(* The hint database contains type size related lemmas *)
Create HintDb typSize.

(* define size of types *)
Fixpoint size_typ (A1 : typ) : nat :=
  match A1 with
    | t_int => 1
    | t_top => 1
    | t_bot => 1
    | t_arrow A2 B1 => 1 + (size_typ A2) + (size_typ B1)
    | t_and A2 B1 => 1 + (size_typ A2) + (size_typ B1)
    | t_or A2 B1 => 1 + (size_typ A2) + (size_typ B1)
  end.

Lemma size_typ_min : forall A1, 1 <= size_typ A1.
Proof.
  intro A. induction A; simpl; lia.
Qed.

#[export] Hint Resolve size_typ_min : typSize.

Lemma typ_size_lg_z : forall T, size_typ T > 0.
Proof.
  introv.
  pose proof (size_typ_min) T.
  inverts~ H.
Qed.

#[export] Hint Resolve typ_size_lg_z : typSize.

Lemma choose_decrease_size : forall m A B,
    size_typ (choose m A B) = size_typ A + size_typ B + 1.
Proof.
  intros; destruct m; simpl in *; lia.
Qed.

Hint Rewrite choose_decrease_size : typSize.

Lemma split_decrease_size: forall m A B C,
    spl m A B C -> size_typ B < size_typ A /\ size_typ C < size_typ A.
Proof with (pose proof (typ_size_lg_z); simpl in *; try lia).
  - introv H.
    induction H; try rewrite choose_decrease_size in *; simpl in *; eauto...
    destruct m; eauto...
    destruct m; eauto...
Qed.

Ltac spl_size :=
  try repeat match goal with
         | [ H: spl _ _ _ _ |- _ ] =>
           ( lets (?&?): split_decrease_size H; clear H)
             end;
  try rewrite choose_decrease_size in *.

(********************************************)
(*                                          *)
(*               Ltac elia                  *)
(*  enhanced lia with split_decrease_size   *)
(*                                          *)
(********************************************)
Ltac elia :=
  try solve [pose proof (typ_size_lg_z);
             spl_size; simpl in *; try lia].

Ltac indTypSize s :=
  assert (SizeInd: exists i, s < i) by eauto with typSize;
  destruct SizeInd as [i SizeInd];
  repeat match goal with | [ h : typ |- _ ] => (gen h) end;
  induction i as [|i IH]; [
    intros; match goal with | [ H : _ < 0 |- _ ] => inverts H end
  | intros ].

author: XSnow

repo: DistributingTypes


text:
Require Import Logic.Class.Eq.

Require Import Logic.STLC.Subst.
Require Import Logic.STLC.Value.
Require Import Logic.STLC.Syntax.
Require Import Logic.STLC.Replace.

Declare Scope STLC_Eval_scope.

(* Big step semantics of STLC                                                   *)
(* EVar: a variable evaluates to itself                                         *)
(* EAnn: if a term evaluates to a value, the annotated term evaluates to same   *)
(* ELam: if a term evaluates to a value, abstracting preserves evaluation       *)
(* EAppN: evaluation for application, neutral case                              *)
(* EAppL: evaluation for application, lambda case                               *)
Inductive Eval (b v:Type)(eq:Eq v) : Exp b v -> Exp b v -> Prop :=
| EVar : forall (x:v), Eval b v eq (Var x) (Var x)
| EAnn : forall (e e':Exp b v) (Ty:T b),
    Value e' -> Eval b v eq e e' -> Eval b v eq (Ann e Ty) e'
| ELam : forall (e e':Exp b v) (x:v),
    Value e' -> Eval b v eq e e' -> Eval b v eq (Lam x e) (Lam x e')
| EAppN : forall (e1 e1' e2 e2':Exp b v),
    Neutral e1'         ->
    Value e2'           ->
    Eval b v eq e1 e1'  ->
    Eval b v eq e2 e2'  ->
    Eval b v eq (App e1 e2) (App e1' e2')
| EAppL : forall (e1 e1' e2 e2':Exp b v) (x:v),
    Value e1'                               ->
    Value e2'                               ->
    Eval b v eq e1 (Lam x e1')              ->
    Eval b v eq (subst (e2 // x) e1') e2'   ->
    Eval b v eq (App e1 e2) e2'
.

Arguments Eval  {b} {v} {eq}.
Arguments EVar  {b} {v} {eq}.
Arguments EAnn  {b} {v} {eq}.
Arguments ELam  {b} {v} {eq}.
Arguments EAppN {b} {v} {eq}.
Arguments EAppL {b} {v} {eq}.

Notation "e >>> e'" := (Eval e e')
    (at level 90, no associativity) : STLC_Eval_scope.

Open Scope STLC_Eval_scope.

author: possientis

repo: Prog

save_path: github-repos/coq/possientis-Prog


text:
(* Law of Excluded Middle *)
Axiom excluded_middle : forall P : Prop, P \/ ~ P.

(* Basic Set Definition *)
Parameter set : Type.

Parameter elem : set -> set -> Prop.
Notation "x 'in' y" := (elem x y) (at level 70).

Definition subset (A B : set) := forall C : set, C in A -> C in B.
Notation "x 'sub' y" := (subset x y) (at level 70).

(* ZF Axioms *)
Axiom extens_ax : forall A B : set,
    (forall C : set, C in A <-> C in B) -> A = B.

Axiom pair_ax : forall A B : set,
    { C : set | forall D, D in C <-> D = A \/ D = B }.

Axiom power_ax : forall A : set, { B : set | forall C, C in B <-> C sub A }.

Axiom empty_ax : { A : set | forall B : set, ~ B in A }.

Axiom union_ax : forall A : set,
    { B : set | forall C : set, C in B <-> (exists D : set, C in D /\ D in A) }.

Axiom sep_ax : forall (P : set -> Prop) (A : set),
    { B : set | forall C : set, C in B <-> C in A /\ P C }.

repo: zf


text:
(* ***********************************************************************)
(*                                                                       *)
(*   Synchronously executed Interpreted Time Petri Nets (SITPNs)         *)
(*                                                                       *)
(*                                                                       *)
(*   Copyright Université de Montpellier, contributor(s): Vincent        *)
(*   Iampietro, David Andreu, David Delahaye (May 2020)                  *)
(*                                                                       *)
(*   This software is governed by the CeCILL-C license under French law  *)
(*   and abiding by the rules of distribution of free software.  You can *)
(*   use, modify and/ or redistribute the software under the terms of    *)
(*   the CeCILL-C license as circulated by CEA, CNRS and INRIA at the    *)
(*   following URL "http://www.cecill.info".  The fact that you are      *)
(*   presently reading this means that you have had knowledge of the     *)
(*   CeCILL-C license and that you accept its terms.                     *)
(*                                                                       *)
(* ***********************************************************************)

(* Import Sitpn material. *)

Require Import simpl.Sitpn.
Require Import simpl.SitpnTokenPlayer.
Require Import simpl.SitpnSemantics.

(* Import falling edge and rising edge completeness lemmas. *)

Require Import simpl.SitpnFallingEdgeComplete.
Require Import simpl.SitpnRisingEdgeComplete.

(* Import lemmas on SITPN and states well-definition. *)

Require Import simpl.SitpnFallingEdgeWellDef.

(** * Completeness proof between [sitpn_cycle] and [SitpnSemantics]. *)

Theorem sitpn_cycle_complete :
  forall (sitpn : Sitpn)
         (s s' s'' : SitpnState)
         (time_value : nat)
         (env : Condition -> nat -> bool),
    IsWellDefinedSitpn sitpn ->
    IsWellDefinedSitpnState sitpn s ->
    IsWellDefinedSitpnState sitpn s' ->
    IsWellDefinedSitpnState sitpn s'' ->
    SitpnSemantics sitpn s s' time_value env falling_edge ->
    SitpnSemantics sitpn s' s'' time_value env rising_edge ->
    exists (istate fstate : SitpnState),
      sitpn_cycle sitpn s time_value env = Some (istate, fstate) /\
      sitpn_state_eq s' istate /\
      sitpn_state_eq s'' fstate.
Proof.
  intros sitpn s s' s'' t env
         Hwell_def_sitpn Hwell_def_s Hwell_def_s' Hwell_def_s''
         Hfall_spec Hrising_spec.

  (* Let's dig the function!! *)
  unfold sitpn_cycle.

  (* Specializes sitpn_falling_edge_complete then rewrites the goal *)

  specialize (sitpn_falling_edge_complete
                sitpn s s' t env Hwell_def_sitpn
                Hwell_def_s Hwell_def_s' Hfall_spec)
    as Hex_fall_fun.
  inversion_clear Hex_fall_fun as (istate & Hw_fall_fun).
  inversion_clear Hw_fall_fun as (Hfall_fun & Hsteq_s'_istate).
  rewrite Hfall_fun.

  (* Specializes sitpn_rising_edge_complete then rewrites the goal. *)

  specialize (sitpn_rising_edge_complete
                sitpn s' s'' t env istate
                Hwell_def_sitpn Hwell_def_s' Hwell_def_s'' Hrising_spec Hsteq_s'_istate)
    as Hex_rising_fun.
  inversion_clear Hex_rising_fun as (fstate & Hw_rising_fun).
  inversion_clear Hw_rising_fun as (Hrising_fun & Hsteq_s''_fs).

  (* Instantiates states and completes the proof. *)
  rewrite Hrising_fun.
  exists istate, fstate.
  apply (conj (eq_refl (Some (istate, fstate))) (conj Hsteq_s'_istate Hsteq_s''_fs)).
Qed.

author: viampietro

repo: sitpns

save_path: github-repos/coq/viampietro-sitpns


text:
(* This program 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 program 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 General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)

(**
   natZ.
   Some lemmas about inject_nat, absolu and the relation between
   Z and nat in general.

   @author Olga Caprotti and Martijn Oostdijk
   @version $Revision$
*)

Require Import ZArith.
Require Import EqNat.

Require Import lemmas.

Lemma abs_opp : forall x : Z, Z.abs_nat x = Z.abs_nat (- x).
Proof.
   simple induction x.
   simpl in |- *. reflexivity.
   simpl in |- *. reflexivity.
   simpl in |- *. reflexivity.
Qed.

Lemma inj_abs_pos : forall x : Z, (x >= 0)%Z -> Z_of_nat (Z.abs_nat x) = x.
Proof.
   simple induction x.
   reflexivity.
   intros. simpl in |- *.
   induction  p as [p Hrecp| p Hrecp| ].
   rewrite BinInt.Zpos_xI.
   rewrite <- Hrecp.
   replace (nat_of_P (xI p)) with (S (2 * nat_of_P p)).
   rewrite Znat.inj_S.
   rewrite Znat.inj_mult.
   rewrite Hrecp.
   simpl in |- *.
   reflexivity.
   apply Z.le_ge. apply Zorder.Zle_0_pos.
   replace 2 with (nat_of_P 2).
   rewrite <- nat_of_P_mult_morphism.
   simpl in |- *.
   rewrite <- nat_of_P_o_P_of_succ_nat_eq_succ.
   rewrite P_of_succ_nat_o_nat_of_P_eq_succ.
   simpl in |- *.
   reflexivity.
   simpl in |- *.
   reflexivity.
   apply Z.le_ge. apply Zorder.Zle_0_pos.
   rewrite BinInt.Zpos_xO.
   rewrite <- Hrecp.
   replace (nat_of_P (xO p)) with (2 * nat_of_P p).
   rewrite Znat.inj_mult.
   rewrite Hrecp.
   simpl in |- *.
   reflexivity.
   apply Z.le_ge. apply Zorder.Zle_0_pos.
   replace 2 with (nat_of_P 2).
   rewrite <- nat_of_P_mult_morphism.
   simpl in |- *.
   reflexivity.
   simpl in |- *.
   reflexivity.
   apply Z.le_ge.
   apply Zorder.Zle_0_pos.
   reflexivity.
   intros.
   elim H.
   simpl in |- *.
   reflexivity.
Qed.

Lemma inj_abs_neg :
 forall x : Z, (x < 0)%Z -> Z_of_nat (Z.abs_nat x) = (- x)%Z.
Proof.
   intros.
   rewrite abs_opp.
   apply inj_abs_pos.
   apply Z.le_ge.
   apply Zplus_le_reg_l with x.
   rewrite <- Zplus_0_r_reverse.
   rewrite Zplus_opp_r.
   apply Zlt_le_weak.
   assumption.
Qed.

Lemma abs_inj : forall n : nat, Z.abs_nat (Z_of_nat n) = n.
Proof.
   simple induction n.
   simpl in |- *. reflexivity.
   intros m IH.
   rewrite <- IH. simpl in |- *.
   rewrite nat_of_P_o_P_of_succ_nat_eq_succ.
   reflexivity.
Qed.

Lemma abs_mult : forall x y : Z, Z.abs_nat (x * y) = Z.abs_nat x * Z.abs_nat y.
Proof.
   simple induction x.
   simpl in |- *. intro. reflexivity.
   intro.
   simple induction y.
   simpl in |- *.
   rewrite <- mult_n_O.
   reflexivity.
   intro.
   simpl in |- *.
   rewrite <- nat_of_P_mult_morphism.
   reflexivity.
   simpl in |- *.
   intro.
   rewrite <- nat_of_P_mult_morphism.
   reflexivity.
   intro.
   simple induction y.
   simpl in |- *.
   rewrite <- mult_n_O.
   reflexivity.
   intro.
   unfold Z.abs_nat in |- *.
   simpl in |- *.
   rewrite <- nat_of_P_mult_morphism.
   reflexivity.
   intro.
   unfold Z.abs_nat in |- *.
   simpl in |- *.
   rewrite <- nat_of_P_mult_morphism.
   reflexivity.
Qed.

Lemma isnat_inj_abs :
 forall (x : Z) (n : nat), x = Z_of_nat n -> n = Z.abs_nat x.
Proof.
   intros.
   rewrite H.
   rewrite abs_inj.
   reflexivity.
Qed.

Lemma isnat_abs_inj :
 forall (x : Z) (n : nat), (0 <= x)%Z -> n = Z.abs_nat x -> x = Z_of_nat n.
Proof.
   intros.
   rewrite H0.
   rewrite inj_abs_pos.
   reflexivity.
   apply Z.le_ge.
   assumption.
Qed.

Lemma isnat_plus : forall x y : Z, (0 <= x)%Z -> (0 <= y)%Z -> (0 <= x + y)%Z.
Proof.
   simple induction x. simpl in |- *. intros. assumption.
   intro. simple induction y. simpl in |- *. intros. assumption.
   simpl in |- *. intros. unfold Z.le in |- *. simpl in |- *. discriminate.
   intros. unfold Z.le in H0. elim H0. simpl in |- *. reflexivity.
   intros. unfold Z.le in H. elim H. simpl in |- *. reflexivity.
Qed.

Lemma isnat_mult : forall x y : Z, (0 <= x)%Z -> (0 <= y)%Z -> (0 <= x * y)%Z.
Proof.
   simple induction x.
   simpl in |- *. intros. unfold Z.le in |- *. simpl in |- *. discriminate.
   intro. simple induction y. simpl in |- *. intros. unfold Z.le in |- *. simpl in |- *. discriminate.
   simpl in |- *. intros. unfold Z.le in |- *. simpl in |- *. discriminate.
   intros. unfold Z.le in H0. elim H0. simpl in |- *. reflexivity.
   intros. unfold Z.le in H. elim H. simpl in |- *. reflexivity.
Qed.

Lemma lezle :
 forall x y : Z,
 (0 <= x)%Z -> (0 <= y)%Z -> (x <= y)%Z -> Z.abs_nat x <= Z.abs_nat y.
Proof.
   intros.
   elim (le_or_lt (Z.abs_nat x) (Z.abs_nat y)).
   intros. assumption.
   intros. elim (Zlt_not_le y x).
   rewrite <- (inj_abs_pos x).
   rewrite <- (inj_abs_pos y).
   apply Znat.inj_lt. assumption.
   apply Z.le_ge. assumption.
   apply Z.le_ge. assumption.
   assumption.
Qed.

Lemma gtzgt :
 forall x y : Z,
 (0 <= x)%Z -> (0 <= y)%Z -> (x > y)%Z -> Z.abs_nat x > Z.abs_nat y.
Proof.
   intros.
   elim (le_or_lt (Z.abs_nat x) (Z.abs_nat y)).
   intros.
   elim (Zle_not_lt x y).
   rewrite <- (inj_abs_pos x).
   rewrite <- (inj_abs_pos y).
   apply Znat.inj_le. assumption.
   apply Z.le_ge. assumption.
   apply Z.le_ge. assumption.
   apply Z.gt_lt. assumption.
   unfold gt in |- *. intro. assumption.
Qed.

Lemma ltzlt :
 forall x y : Z,
 (0 <= x)%Z -> (0 <= y)%Z -> (x < y)%Z -> Z.abs_nat x < Z.abs_nat y.
Proof.
   intros.
   change (Z.abs_nat y > Z.abs_nat x) in |- *.
   apply gtzgt. assumption. assumption.
   apply Z.lt_gt. assumption.
Qed.

Lemma abs_plus_pos :
 forall x y : Z,
 (0 <= x)%Z -> (0 <= y)%Z -> Z.abs_nat (x + y) = Z.abs_nat x + Z.abs_nat y.
Proof.
   simple induction x.
   simpl in |- *.
   intros.
   reflexivity.
   intro.
   simple induction y.
   simpl in |- *.
   rewrite <- plus_n_O.
   intros.
   reflexivity.
   simpl in |- *.
   intros.
   apply nat_of_P_plus_morphism.
   intros.
   unfold Z.le in H0.
   simpl in H0.
   elim H0.
   reflexivity.
   intros.
   unfold Z.le in H.
   simpl in H.
   elim H.
   reflexivity.
Qed.

Lemma abs_minus_pos :
 forall x y : Z,
 (0 <= x)%Z ->
 (0 <= y)%Z -> (x >= y)%Z -> Z.abs_nat (x - y) = Z.abs_nat x - Z.abs_nat y.
Proof.
   intros.
   elim (Z_of_nat_complete x).
   intros nx Hx.
   elim (Z_of_nat_complete y).
   intros ny Hy.
   elim (Z_of_nat_complete (x - y)).
   intros d Hd.
   rewrite Hx.
   rewrite Hy.
   rewrite <- Znat.inj_minus1.
   rewrite abs_inj.
   rewrite abs_inj.
   rewrite abs_inj.
   reflexivity.
   rewrite (isnat_inj_abs x nx).
   rewrite (isnat_inj_abs y ny).
   apply lezle.
   assumption.
   assumption.
   apply Z.ge_le.
   assumption.
   assumption.
   assumption.
   unfold Zminus in |- *.
   apply Zle_left.
   apply Z.ge_le.
   assumption.
   assumption.
   assumption.
Qed.

Lemma abs_pred_pos :
 forall x : Z, (0 < x)%Z -> pred (Z.abs_nat x) = Z.abs_nat (x - 1).
Proof.
   intros.
   rewrite abs_minus_pos.
   replace (Z.abs_nat 1) with 1.
   rewrite predminus1.
   reflexivity.
   reflexivity.
   apply Zlt_le_weak.
   assumption.
   unfold Z.le in |- *.
   simpl in |- *.
   discriminate.
   apply Z.le_ge.
   change (Z.succ 0 <= x)%Z in |- *.
   apply Zlt_le_succ.
   assumption.
Qed.

Lemma abs_neq_lt : forall x : Z, x <> 0%Z -> 0 < Z.abs_nat x.
Proof.
   simple induction x.
   intro. elim H. reflexivity.
   intros. change (Z.abs_nat 0 < Z.abs_nat (Zpos p)) in |- *. apply ltzlt.
   unfold Z.le in |- *. simpl in |- *. discriminate.
   unfold Z.le in |- *. simpl in |- *. discriminate.
   unfold Z.lt in |- *. simpl in |- *. reflexivity.
   intros. change (Z.abs_nat 0 < Z.abs_nat (Zpos p)) in |- *. apply ltzlt.
   unfold Z.le in |- *. simpl in |- *. discriminate.
   unfold Z.le in |- *. simpl in |- *. discriminate.
   unfold Z.lt in |- *. simpl in |- *. reflexivity.
Qed.

Lemma nat_ge_0 : forall n : nat, (Z_of_nat n >= 0)%Z.
Proof.
   simple induction n.
   simpl in |- *. unfold Z.ge in |- *. simpl in |- *. discriminate.
   intros m IHm.
   change (Z_of_nat (S m) >= Z_of_nat 0)%Z in |- *.
   apply Znat.inj_ge. unfold ge in |- *.
   apply le_O_n.
Qed.

author: coq-community

repo: pocklington


(* ** License
 * -----------------------------------------------------------------------
 * Copyright 2016--2017 IMDEA Software Institute
 * Copyright 2016--2017 Inria
 *
 * Permission is hereby granted, free of charge, to any person obtaining
 * a copy of this software and associated documentation files (the
 * "Software"), to deal in the Software without restriction, including
 * without limitation the rights to use, copy, modify, merge, publish,
 * distribute, sublicense, and/or sell copies of the Software, and to
 * permit persons to whom the Software is furnished to do so, subject to
 * the following conditions:
 *
 * The above copyright notice and this permission notice shall be
 * included in all copies or substantial portions of the Software.
 *
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
 * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
 * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
 * IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY
 * CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,
 * TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE
 * SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 * ----------------------------------------------------------------------- *)

(* ** Imports and settings *)
From CoqWord Require Import ssrZ.
Require Import expr ZArith psem.
Import all_ssreflect all_algebra.
Import Utf8.
Import oseq.

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

Local Open Scope seq_scope.
Local Open Scope vmap_scope.
Local Open Scope Z_scope.
(* -------------------------------------------------------------------------- *)
(* ** Smart constructors                                                      *)
(* -------------------------------------------------------------------------- *)

Definition sword_of_int sz (e: pexpr) :=
  Papp1 (Oword_of_int sz) e.

Definition sint_of_word sz (e: pexpr) :=
  if is_wconst sz e is Some w
  then Pconst (wunsigned w)
  else Papp1 (Oint_of_word sz) e.

Definition ssign_extend sz sz' (e: pexpr) :=
  if is_wconst sz' e is Some w
  then Papp1 (Oword_of_int sz) (Pconst (wunsigned (sign_extend sz w)))
  else Papp1 (Osignext sz sz') e.

Definition szero_extend sz sz' (e: pexpr) :=
  if is_wconst sz' e is Some w
  then Papp1 (Oword_of_int sz) (Pconst (wunsigned (zero_extend sz w)))
  else Papp1 (Ozeroext sz sz') e.

Definition snot_bool (e:pexpr) :=
  match e with
  | Pbool b      => negb b
  | Papp1 Onot e => e
  | _            => Papp1 Onot e
  end.

Definition snot_w (sz: wsize) (e:pexpr) :=
  match is_wconst sz e with
  | Some n => wconst (wnot n)
  | None   => Papp1 (Olnot sz) e
  end.

Definition sneg_int (e: pexpr) :=
  match e with
  | Pconst z => Pconst (- z)
  | Papp1 (Oneg Op_int) e' => e'
  | _ => Papp1 (Oneg Op_int) e
  end.

Definition sneg_w (sz: wsize) (e:pexpr) :=
  match is_wconst sz e with
  | Some n => wconst (- n)%R
  | None   => Papp1 (Oneg (Op_w sz)) e
  end.

Definition s_op1 o e :=
  match o with
  | Oword_of_int sz => sword_of_int sz e
  | Oint_of_word sz => sint_of_word sz e
  | Osignext sz sz' => ssign_extend sz sz' e
  | Ozeroext sz sz' => szero_extend sz sz' e
  | Onot  => snot_bool e
  | Olnot sz => snot_w sz e
  | Oneg Op_int => sneg_int e
  | Oneg (Op_w sz) => sneg_w sz e
  end.

(* ------------------------------------------------------------------------ *)
Definition sand e1 e2 :=
  match is_bool e1, is_bool e2 with
  | Some b, _ => if b then e2 else false
  | _, Some b => if b then e1 else false
  | _, _      => Papp2 Oand e1 e2
  end.

Definition sor e1 e2 :=
   match is_bool e1, is_bool e2 with
  | Some b, _ => if b then Pbool true else e2
  | _, Some b => if b then Pbool true else e1
  | _, _       => Papp2 Oor e1 e2
  end.

(* ------------------------------------------------------------------------ *)

Definition sadd_int e1 e2 :=
  match is_const e1, is_const e2 with
  | Some n1, Some n2 => Pconst (n1 + n2)
  | Some n, _ =>
    if (n == 0)%Z then e2 else Papp2 (Oadd Op_int) e1 e2
  | _, Some n =>
    if (n == 0)%Z then e1 else Papp2 (Oadd Op_int) e1 e2
  | _, _ => Papp2 (Oadd Op_int) e1 e2
  end.

Definition sadd_w sz e1 e2 :=
  match is_wconst sz e1, is_wconst sz e2 with
  | Some n1, Some n2 => wconst (n1 + n2)
  | Some n, _ => if n == 0%R then e2 else Papp2 (Oadd (Op_w sz)) e1 e2
  | _, Some n => if n == 0%R then e1 else Papp2 (Oadd (Op_w sz)) e1 e2
  | _, _ => Papp2 (Oadd (Op_w sz)) e1 e2
  end.

Definition sadd ty :=
  match ty with
  | Op_int => sadd_int
  | Op_w sz => sadd_w sz
  end.

Definition ssub_int e1 e2 :=
  match is_const e1, is_const e2 with
  | Some n1, Some n2 => Pconst (n1 - n2)
  | _, Some n =>
    if (n == 0)%Z then e1 else Papp2 (Osub Op_int) e1 e2
  | _, _ => Papp2 (Osub Op_int) e1 e2
  end.

Definition ssub_w sz e1 e2 :=
  match is_wconst sz e1, is_wconst sz e2 with
  | Some n1, Some n2 => wconst (n1 - n2)
  | _, Some n => if n == 0%R then e1 else Papp2 (Osub (Op_w sz)) e1 e2
  | _, _ => Papp2 (Osub (Op_w sz)) e1 e2
  end.

Definition ssub ty :=
  match ty with
  | Op_int => ssub_int
  | Op_w sz => ssub_w sz
  end.

Definition smul_int e1 e2 :=
  match is_const e1, is_const e2 with
  | Some n1, Some n2 => Pconst (n1 * n2)
  | Some n, _ =>
    if (n == 0)%Z then Pconst 0
    else if (n == 1)%Z then e2
    else Papp2 (Omul Op_int) e1 e2
  | _, Some n =>
    if (n == 0)%Z then Pconst 0
    else if (n == 1)%Z then e1
    else Papp2 (Omul Op_int) e1 e2
  | _, _ => Papp2 (Omul Op_int) e1 e2
  end.

Definition smul_w sz e1 e2 :=
  match is_wconst sz e1, is_wconst sz e2 with
  | Some n1, Some n2 => wconst (n1 * n2)
  | Some n, _ =>
    if n == 0%R then @wconst sz 0
    else if n == 1%R then e2
    else Papp2 (Omul (Op_w sz)) (wconst n) e2
  | _, Some n =>
    if n == 0%R then @wconst sz 0
    else if n == 1%R then e1
    else Papp2 (Omul (Op_w sz)) e1 (wconst n)
  | _, _ => Papp2 (Omul (Op_w sz)) e1 e2
  end.

Definition smul ty :=
  match ty with
  | Op_int => smul_int
  | Op_w sz => smul_w sz
  end.

Definition s_eq ty e1 e2 :=
  if eq_expr e1 e2 then Pbool true
  else
    match ty with
    | Op_int =>
      match is_const e1, is_const e2 with
      | Some i1, Some i2 => Pbool (i1 == i2)
      | _, _             => Papp2 (Oeq ty) e1 e2
      end
    | Op_w sz =>
      match is_wconst sz e1, is_wconst sz e2 with
      | Some i1, Some i2 => Pbool (i1 == i2)
      | _, _             => Papp2 (Oeq ty) e1 e2
      end
    end.

Definition sneq ty e1 e2 :=
  match is_bool (s_eq ty e1 e2) with
  | Some b => Pbool (~~ b)
  | None      => Papp2 (Oneq ty) e1 e2
  end.

Definition is_cmp_const (ty: cmp_kind) (e: pexpr) : option Z :=
  match ty with
  | Cmp_int => is_const e
  | Cmp_w sg sz =>
    is_wconst sz e >>= λ w,
    Some match sg with
    | Signed => wsigned w
    | Unsigned => wunsigned w
    end
  end%O.

Definition slt ty e1 e2 :=
  if eq_expr e1 e2 then Pbool false
  else match is_cmp_const ty e1, is_cmp_const ty e2 with
  | Some n1, Some n2 => Pbool (n1 <? n2)%Z
  | _      , _       => Papp2 (Olt ty) e1 e2
  end.

Definition sle ty e1 e2 :=
  if eq_expr e1 e2 then Pbool true
  else match is_cmp_const ty e1, is_cmp_const ty e2 with
  | Some n1, Some n2 => Pbool (n1 <=? n2)%Z
  | _      , _       => Papp2 (Ole ty) e1 e2
  end.

Definition sgt ty e1 e2 :=
  if eq_expr e1 e2 then Pbool false
  else match is_cmp_const ty e1, is_cmp_const ty e2 with
  | Some n1, Some n2 => Pbool (n1 >? n2)%Z
  | _      , _       => Papp2 (Ogt ty) e1 e2
  end.

Definition sge ty e1 e2 :=
  if eq_expr e1 e2 then Pbool true
  else match is_cmp_const ty e1, is_cmp_const ty e2 with
  | Some n1, Some n2 => Pbool (n1 >=? n2)%Z
  | _      , _       => Papp2 (Oge ty) e1 e2
  end.

Definition sbitw i (z: ∀ sz, word sz → word sz → word sz) sz e1 e2 :=
  match is_wconst sz e1, is_wconst sz e2 with
  | Some n1, Some n2 => wconst (z sz n1 n2)
  | _, _ => Papp2 (i sz) e1 e2
  end.

Definition soint i f e1 e2 :=
  match is_const e1, is_const e2 with
  | Some n1, Some n2 =>  Pconst (f n1 n2)
  | _, _ => Papp2 (i Cmp_int) e1 e2
  end.

Definition sbituw i (z: signedness -> ∀ sz, word sz → word sz → word sz) u sz e1 e2 :=
  match is_wconst sz e1, is_wconst sz e2 with
  | Some n1, Some n2 =>
    if n2 == 0%R then Papp2 (i (Cmp_w u sz)) e1 e2
    else wconst (z u sz n1 n2)
  | _, _ => Papp2 (i (Cmp_w u sz)) e1 e2
  end.

Definition sdiv ty (e1 e2:pexpr) :=
  match ty with
  | Cmp_int => soint Odiv Z.div e1 e2
  | Cmp_w u sz => sbituw Odiv (signed (@wdiv) (@wdivi)) u sz e1 e2
  end.

Definition smod ty e1 e2 :=
  match ty with
  | Cmp_int => soint Omod Z.modulo e1 e2
  | Cmp_w u sz => sbituw Omod (signed (@wmod) (@wmodi)) u sz e1 e2
  end.

(* TODO: could be improved when one operand is known *)
Definition sland := sbitw Oland (@wand).
Definition slor := sbitw Olor (@wor).
Definition slxor := sbitw Olxor (@wxor).

Definition sbitw8 i (z: ∀ sz, word sz → u8 → word sz) sz e1 e2 :=
  match is_wconst sz e1, is_wconst U8 e2 with
  | Some n1, Some n2 => wconst (z sz n1 n2)
  | _, _ => Papp2 (i sz) e1 e2
  end.

Definition sshr sz e1 e2 :=
  sbitw8 Olsr (@sem_shr) sz e1 e2.

Definition sshl sz e1 e2 :=
   sbitw8 Olsl (@sem_shl) sz e1 e2.

Definition ssar sz e1 e2 :=
  sbitw8 Oasr (@sem_sar) sz e1 e2.

Definition svadd ve sz e1 e2 :=
   sbitw (Ovadd ve) (@sem_vadd ve) sz e1 e2.

Definition svsub ve sz e1 e2 :=
   sbitw (Ovsub ve) (@sem_vsub ve) sz e1 e2.

Definition svmul ve sz e1 e2 :=
  sbitw (Ovmul ve) (@sem_vmul ve) sz e1 e2.

Definition svshr ve sz e1 e2 :=
  sbitw8 (Ovlsr ve) (@sem_vshr ve) sz e1 e2.

Definition svshl ve sz e1 e2 :=
   sbitw8 (Ovlsl ve) (@sem_vshl ve) sz e1 e2.

Definition svsar ve sz e1 e2 :=
  sbitw8 (Ovasr ve) (@sem_vsar ve) sz e1 e2.

Definition s_op2 o e1 e2 :=
  match o with
  | Oand    => sand e1 e2
  | Oor     => sor  e1 e2
  | Oadd ty => sadd ty e1 e2
  | Osub ty => ssub ty e1 e2
  | Omul ty => smul ty e1 e2
  | Odiv ty => sdiv ty e1 e2
  | Omod ty => smod ty e1 e2
  | Oeq  ty => s_eq ty e1 e2
  | Oneq ty => sneq ty e1 e2
  | Olt  ty => slt  ty e1 e2
  | Ole  ty => sle  ty e1 e2
  | Ogt  ty => sgt  ty e1 e2
  | Oge  ty => sge  ty e1 e2
  | Oland sz => sland sz e1 e2
  | Olor sz => slor sz e1 e2
  | Olxor sz => slxor sz e1 e2
  | Olsr sz => sshr sz e1 e2
  | Olsl sz => sshl sz e1 e2
  | Oasr sz => ssar sz e1 e2
  | Ovadd ve sz => svadd ve sz e1 e2
  | Ovsub ve sz => svsub ve sz e1 e2
  | Ovmul ve sz => svmul ve sz e1 e2
  | Ovlsr ve sz => svshr ve sz e1 e2
  | Ovlsl ve sz => svshl ve sz e1 e2
  | Ovasr ve sz => svsar ve sz e1 e2
  end.

Definition force_int e :=
  if e is Pconst z then ok (Vint z) else type_error.

Definition s_opN op es :=
  match mapM force_int es >>= sem_opN op with
  | Ok (Vword sz w) => Papp1 (Oword_of_int sz) (Pconst (wunsigned w))
  | _ => PappN op es
  end.

Definition s_if t e e1 e2 :=
  match is_bool e with
  | Some b => if b then e1 else e2
  | None   => Pif t e e1 e2
  end.

(* ** constant propagation
 * -------------------------------------------------------------------- *)

Variant const_v :=
  | Cint of Z
  | Cword sz `(word sz).

Definition const_v_beq (c1 c2: const_v) : bool :=
  match c1, c2 with
  | Cint z1, Cint z2 => z1 == z2
  | Cword sz1 w1, Cword sz2 w2 =>
    match wsize_eq_dec sz1 sz2 with
    | left e => eq_rect _ word w1 _ e == w2
    | _ => false
    end
  | _, _ => false
  end.

Lemma const_v_eq_axiom : Equality.axiom const_v_beq.
Proof.
case => [ z1 | sz1 w1 ] [ z2 | sz2 w2] /=; try (constructor; congruence).
+ case: eqP => [ -> | ne ]; constructor; congruence.
case: wsize_eq_dec => [ ? | ne ]; last (constructor; congruence).
subst => /=.
by apply:(iffP idP) => [ /eqP | [] ] ->.
Qed.

Definition const_v_eqMixin     := Equality.Mixin const_v_eq_axiom.
Canonical  const_v_eqType      := Eval hnf in EqType const_v const_v_eqMixin.

Local Notation cpm := (Mvar.t const_v).

Definition const v :=
  match v with
  | Cint z  => Pconst z
  | Cword sz z => wconst z
  end.

Fixpoint const_prop_e (m:cpm) e :=
  match e with
  | Pconst _
  | Pbool  _
  | Parr_init _
    => e
  | Pvar  x       => if Mvar.get m x is Some n then const n else e
  | Pglobal _     => e
  | Pget  sz x e  => Pget  sz x (const_prop_e m e)
  | Pload sz x e  => Pload sz x (const_prop_e m e)
  | Papp1 o e     => s_op1 o (const_prop_e m e)
  | Papp2 o e1 e2 => s_op2 o (const_prop_e m e1)  (const_prop_e m e2)
  | PappN op es   => s_opN op (map (const_prop_e m) es)
  | Pif t e e1 e2 => s_if t (const_prop_e m e) (const_prop_e m e1) (const_prop_e m e2)
  end.

Definition empty_cpm : cpm := @Mvar.empty const_v.

Definition merge_cpm : cpm -> cpm -> cpm :=
  Mvar.map2 (fun _ (o1 o2: option const_v) =>
   match o1, o2 with
   | Some n1, Some n2 =>
     if (n1 == n2)%Z then Some n1
     else None
   | _, _ => None
   end).

Definition remove_cpm (m:cpm) (s:Sv.t): cpm :=
  Sv.fold (fun x m => Mvar.remove m x) s m.

Definition const_prop_rv (m:cpm) (rv:lval) : cpm * lval :=
  match rv with
  | Lnone _ _    => (m, rv)
  | Lvar  x      => (Mvar.remove m x, rv)
  | Lmem  sz x e => (m, Lmem sz x (const_prop_e m e))
  | Laset sz x e => (Mvar.remove m x, Laset sz x (const_prop_e m e))
  end.

Fixpoint const_prop_rvs (m:cpm) (rvs:lvals) : cpm * lvals :=
  match rvs with
  | [::] => (m, [::])
  | rv::rvs =>
    let (m,rv)  := const_prop_rv m rv in
    let (m,rvs) := const_prop_rvs m rvs in
    (m, rv::rvs)
  end.

Definition wsize_of_stype (ty: stype) : wsize :=
  if ty is sword sz then sz else U64.

Definition add_cpm (m:cpm) (rv:lval) tag ty e :=
  if rv is Lvar x then
    if tag is AT_inline then
      match e with
      | Pconst z =>  Mvar.set m x (Cint z)
      | Papp1 (Oword_of_int sz') (Pconst z) =>
        let szty := wsize_of_stype ty in
        let w := zero_extend szty (wrepr sz' z) in
        let w :=
            let szx := wsize_of_stype (vtype x) in
            if (szty ≤ szx)%CMP
            then Cword w
            else Cword (zero_extend szx w) in
        Mvar.set m x w
      | _ => m
      end
    else m
  else m.

Section CMD.

  Variable const_prop_i : cpm -> instr -> cpm * cmd.

  Fixpoint const_prop (m:cpm) (c:cmd) : cpm * cmd :=
    match c with
    | [::] => (m, [::])
    | i::c =>
      let (m,ic) := const_prop_i m i in
      let (m, c) := const_prop m c in
      (m, ic ++ c)
    end.

End CMD.

Fixpoint const_prop_ir (m:cpm) ii (ir:instr_r) : cpm * cmd :=
  match ir with
  | Cassgn x tag ty e =>
    let e := const_prop_e m e in
    let (m,x) := const_prop_rv m x in
    let m := add_cpm m x tag ty e in
    (m, [:: MkI ii (Cassgn x tag ty e)])

  | Copn xs t o es =>
    (* TODO: Improve this *)
    let es := map (const_prop_e m) es in
    let (m,xs) := const_prop_rvs m xs in
    (m, [:: MkI ii (Copn xs t o es) ])

  | Cif b c1 c2 =>
    let b := const_prop_e m b in
    match is_bool b with
    | Some b =>
      let c := if b then c1 else c2 in
      const_prop const_prop_i m c
    | None =>
      let (m1,c1) := const_prop const_prop_i m c1 in
      let (m2,c2) := const_prop const_prop_i m c2 in
      (merge_cpm m1 m2, [:: MkI ii (Cif b c1 c2) ])
    end

  | Cfor x (dir, e1, e2) c =>
    let e1 := const_prop_e m e1 in
    let e2 := const_prop_e m e2 in
    let m := remove_cpm m (write_i ir) in
    let (_,c) := const_prop const_prop_i m c in
    (m, [:: MkI ii (Cfor x (dir, e1, e2) c) ])

  | Cwhile a c e c' =>
    let m := remove_cpm m (write_i ir) in
    let (m',c) := const_prop const_prop_i m c in
    let e := const_prop_e m' e in
    let (_,c') := const_prop const_prop_i m' c' in
    let cw :=
      match is_bool e with
      | Some false => c
      | _          => [:: MkI ii (Cwhile a c e c')]
      end in
    (m', cw)
  | Ccall fi xs f es =>
    let es := map (const_prop_e m) es in
    let (m,xs) := const_prop_rvs m xs in
    (m, [:: MkI ii (Ccall fi xs f es) ])
  end

with const_prop_i (m:cpm) (i:instr) : cpm * cmd :=
  let (ii,ir) := i in
  const_prop_ir m ii ir.

Definition const_prop_fun (f:fundef) :=
  let (ii,tin,p,c,tout,r) := f in
  let (_, c) := const_prop const_prop_i empty_cpm c in
  MkFun ii tin p c tout r.

Definition const_prop_prog (p:prog) : prog := map_prog const_prop_fun p.


text:
(** * Skeleton of app that asks for GPS and a list of MBTA busses, and displays the ones near you *)
Require Import Coq.Strings.Ascii Coq.Program.Basics Coq.Strings.String.
Require Import Coq.Lists.List Coq.Sorting.Mergesort.
Require Import FunctionApp FunctionAppLemmas FunctionAppTactics.
Require Import TrustedTickBox Common.
Import ListNotations.

Local Open Scope program_scope.

Module Type GPSCoordinateType.
  Axiom t : Type.
  Axiom distance : t -> t -> nat.
  Axiom toString : t -> string.
  Axiom initGPS : t.
End GPSCoordinateType.

(** We implement the following diagram:

<<

                        receive bus list      System Clock (tick)
                              │                    │
                              V                    V
                      ┌────────────────────────────────────────────────────┐
                      │       │                    ├──────┐                │
                      │       V                    V      │                │
    update busses     │    ┌────┐ want busses   ┌──────┐  │                │
    --------------->  │ -> │    │ ------------> │ Bus  │  │ request busses │
                      │    │    │               │ Tick │ ----------------> │ --> internet
    update gps        │    │    │ <------------ │ Box  │  │                │
    --------------->  │ -> │    │ ------------> │      │  │                │
                      │    │    │               └──────┘  │                │
                      │    │ UI │                  ┌──────┘                │
    set max dist      │    │    │                  V                       │
    --------------->  │ -> │    │ want GPS      ┌──────┐                   │
                      │    │    │ ------------> │ GPS  │    request GPS    │
    console out       │    │    │               │ Tick │ ----------------> │--> GPS
    <---------------  │ <- │    │ <------------ │ Box  │                   │
                      │    └────┘ ------------> │      │                   │
                      │       ^                 └──────┘                   │
                      │       │                                            │
                      └────────────────────────────────────────────────────┘
                              ^
                              │
                        receive GPS
>>

    We will eventually want to add knobs for setting the parameters of
    the tick boxes.  The unlabeled double-way arrows are helpers for
    the tick boxes.  *)

Module MBTARequester (GPS : GPSCoordinateType).
  Local Notation GPSCoordinate := GPS.t.

  Module TotalLeBool'StringGPS <: Orders.TotalLeBool'.
    Definition t := (string * GPS.t * nat)%type.
    Definition leb (x y : t) := NatOrder.leb (snd x) (snd y).
    Definition leb_total (x y : t) : leb x y = true \/ leb y x = true
      := NatOrder.leb_total _ _.
  End TotalLeBool'StringGPS.

  Module SortGPSString := Sort TotalLeBool'StringGPS.
  Local Notation sort := SortGPSString.sort.

  Section components.
    Section ui.
      Inductive uiInput :=
      | uiRequestUpdate : uiInput
      | uiSetMaxDist : nat -> uiInput
      | uiGotGPS : GPSCoordinate -> uiInput
      | uiGotBusses : list (string * GPSCoordinate) -> uiInput.

      Inductive uiOutput :=
      | uiOutRequestGPSUpdate
      | uiOutRequestBusUpdate
      | uiConsoleOut (text : string).

      Context (world : Type)
              (handle : uiOutput -> action world).

      Definition newline := "010"%char.

      Definition dump (busList : list (string * GPSCoordinate)) : string
        := fold_right append ""%string
                      (map (fun p => (fst p ++ ": " ++ GPS.toString (snd p) ++ String newline ""))
                           busList)%string.

      Record state :=
        {
          curGPS : GPSCoordinate;
          curBusList : list (string * GPSCoordinate);
          curMaxDist : nat
        }.

      Definition initState : state :=
        {| curGPS := GPS.initGPS;
           curBusList := [];
           curMaxDist := 0 |}.

      Definition setGPS (st : state) (newGPS : GPSCoordinate) : state
        := {| curGPS := newGPS;
              curBusList := st.(curBusList);
              curMaxDist := st.(curMaxDist) |}.

      Definition setBusList (st : state) newBusList : state
        := {| curGPS := st.(curGPS);
              curBusList := newBusList;
              curMaxDist := st.(curMaxDist) |}.

      Definition setMaxDist (st : state) newMaxDist : state
        := {| curGPS := st.(curGPS);
              curBusList := st.(curBusList);
              curMaxDist := newMaxDist |}.

      Definition getInterestingBusses (st : state) : list (string * GPSCoordinate)
        := map
             (@fst _ _)
             (sort (filter
                      (fun scd => let dist := snd scd in
                                  NatOrder.leb dist st.(curMaxDist))
                      (map
                         (fun sc => let coord := snd sc in
                                    (sc, GPS.distance coord st.(curGPS)))
                         st.(curBusList)))).

      Definition dumpState : state -> string :=
        dump ∘ getInterestingBusses.

      (** Separate out the body, so that the proof at the end compiles faster. *)
      Definition uiLoopBody
                 (uiLoop : state -> process uiInput world)
                 (st : state)
                 (sinput := uiInput)
                 (sworld := world)
      : sinput -> action sworld * process sinput sworld
        := fun i =>
             match i with

               | uiRequestUpdate
                 => (handle uiOutRequestGPSUpdate ∘ handle uiOutRequestBusUpdate, uiLoop st)

               | uiSetMaxDist newDist
                 => (id, uiLoop (setMaxDist st newDist))

               | uiGotGPS newGPS
                 => let st' := setGPS st newGPS in
                    (handle (uiConsoleOut (dumpState st')), uiLoop st')

               | uiGotBusses newBusList
                 => let st' := setBusList st newBusList in
                    (handle (uiConsoleOut (dumpState st')), uiLoop st')

             end.

      CoFixpoint uiLoop (st : state) :=
        Step (uiLoopBody uiLoop st).

      Definition ui : process _ _ := uiLoop initState.

    End ui.

    Definition getStep {input output} (p : process input output) :=
      match p with
        | Step f => f
      end.

    Section mbta.
      Inductive mbtaOutput :=
      | mbtaOutRequestGPSUpdate
      | mbtaOutRequestBussesUpdate
      | mbtaConsoleOut (text : string).

      Context (world : Type)
              (handle : mbtaOutput -> action world).

      Inductive mbtaMessage :=
      | mbtaBadState
      | mbtaRequestGPS
      | mbtaRequestBusses
      | mbtaTbGPSRequestDataUpdate
      | mbtaTbBussesRequestDataUpdate.

      Inductive mbtaInput :=
      | mbtaRequestUpdate : mbtaInput
      | mbtaSetMaxDist : nat -> mbtaInput
      | mbtaRecvGPS : GPSCoordinate -> mbtaInput
      | mbtaRecvBusses : list (string * GPSCoordinate) -> mbtaInput
      | mbtaTick (extraTicks : nat).

      Definition mbtaLoopBody
                 (mbtaLoop : forall
                               (ui : process uiInput (stackWorld mbtaMessage world))
                               (tbGPS
                                  tbBusses : process (tbInput unit)
                                                     (stackWorld mbtaMessage world)),
                               stackProcess mbtaMessage mbtaInput world)
                 (ui : process uiInput (stackWorld mbtaMessage world))
                 (tbGPS
                    tbBusses : process (tbInput unit)
                                       (stackWorld mbtaMessage world))
                 (sinput := (mbtaMessage + mbtaInput)%type)
                 (sworld := stackWorld mbtaMessage world)
      : sinput -> action sworld * process sinput sworld
        := (fun i =>
              match i with
                | inl mbtaBadState =>
                  (stackPush mbtaBadState, mbtaLoop ui tbGPS tbBusses)
                | inl mbtaRequestGPS =>
                  let (a, tbGPS') := getStep tbGPS (inr (tbNotifyChange unit)) in
                  (a, mbtaLoop ui tbGPS' tbBusses)
                | inl mbtaRequestBusses =>
                  let (a, tbGPS') := getStep tbGPS (inr (tbNotifyChange unit)) in
                  (a, mbtaLoop ui tbGPS' tbBusses)
                | inl mbtaTbGPSRequestDataUpdate =>
                  (** We can just say that we're immediately ready with a value *)
                  let (a, tbGPS') := getStep tbGPS (inr (tbValueReady tt)) in
                  (a, mbtaLoop ui tbGPS' tbBusses)
                | inl mbtaTbBussesRequestDataUpdate =>
                  (** We can just say that we're immediately ready with a value *)
                  let (a, tbBusses') := getStep tbBusses (inr (tbValueReady tt)) in
                  (a, mbtaLoop ui tbGPS tbBusses')
                | inr (mbtaTick extraTicks) =>
                  let (a, tbGPS') := getStep tbGPS (inr (tbTick unit extraTicks)) in
                  let (a', tbBusses') := getStep tbBusses (inr (tbTick unit extraTicks)) in
                  (a' ∘ a, mbtaLoop ui tbGPS' tbBusses')
                | inr mbtaRequestUpdate =>
                  let (a, ui') := getStep ui uiRequestUpdate in
                  (a, mbtaLoop ui' tbGPS tbBusses)
                | inr (mbtaSetMaxDist d) =>
                  let (a, ui') := getStep ui (uiSetMaxDist d) in
                  (a, mbtaLoop ui' tbGPS tbBusses)
                | inr (mbtaRecvGPS c) =>
                  let (a, ui') := getStep ui (uiGotGPS c) in
                  (a, mbtaLoop ui' tbGPS tbBusses)
                | inr (mbtaRecvBusses c) =>
                  let (a, ui') := getStep ui (uiGotBusses c) in
                  (a, mbtaLoop ui' tbGPS tbBusses)
              end).

      CoFixpoint mbtaLoop ui tbGPS tbBusses
      : stackProcess mbtaMessage mbtaInput world :=
        Step (mbtaLoopBody mbtaLoop ui tbGPS tbBusses).

      Lemma mbtaLoop_eta ui tbGPS tbBusses
      : mbtaLoop ui tbGPS tbBusses = Step (mbtaLoopBody mbtaLoop ui tbGPS tbBusses).
      Proof.
        rewrite stackProcess_eta at 1; reflexivity.
      Qed.

      Definition uiHandler
        := (fun s => match s with
                       | uiOutRequestGPSUpdate => stackPush mbtaRequestGPS
                       | uiOutRequestBusUpdate => stackPush mbtaRequestBusses
                       | uiConsoleOut text => stackLift (handle (mbtaConsoleOut text))
                     end).

      Definition gpsHandler
        := (fun s : tbOutput unit
            => match s with
                 | inl (tbWarnInvalidEvent _ _) => stackPush mbtaBadState
                 | inr tbRequestDataUpdate => stackPush mbtaRequestGPS
                 | inr (tbPublishUpdate _) => stackLift (handle mbtaOutRequestGPSUpdate)
                 | inl _ => stackLift id
               end).

      Definition bussesHandler
        := (fun s : tbOutput unit
            => match s with
                 | inl (tbWarnInvalidEvent _ _) => stackPush mbtaBadState
                 | inr tbRequestDataUpdate => stackPush mbtaRequestBusses
                 | inr (tbPublishUpdate _) => stackLift (handle mbtaOutRequestBussesUpdate)
                 | inl _ => stackLift id
               end).

      Definition mkMBTAStack
                 (ui :
                    forall {world'}
                           (handle : uiOutput -> action world'),
                      process uiInput world')
                 (tbGPS :
                    forall {world'}
                           (handle : tbOutput unit -> action world'),
                      process (tbInput unit) world')
                 (tbBusses :
                    forall {world'}
                           (handle : tbOutput unit -> action world'),
                      process (tbInput unit) world')
      : stackProcess mbtaMessage mbtaInput world :=
        mbtaLoop
          (ui uiHandler)
          (tbGPS gpsHandler)
          (tbBusses bussesHandler).

      Definition mbtaStack := mkMBTAStack ui
                                          (fun world handle => tickBox handle)
                                          (fun world handle => tickBox handle).

      CoFixpoint mbtaGood' uiSt gpsSt bussesSt
      : emptiesStackForever (Step (mbtaLoopBody mbtaLoop
                                                (uiLoop (stackWorld mbtaMessage world) uiHandler uiSt)
                                                (tickBoxLoop gpsHandler gpsSt)
                                                (tickBoxLoop bussesHandler bussesSt))).
      Proof.
        destruct gpsSt as [[]], bussesSt as [[]];
        constructor;
        let tac := (idtac;
                    match goal with
                      | [ |- appcontext[if ?E then _ else _] ]
                        => (let T := type of E in
                            constr_eq T bool;
                            case_eq E; intro)
                    end) in
        emptiesStackForever_t mbtaGood' mbtaInput (@mbtaLoop_eta) (@mbtaLoop) tac.
      Qed.

      Lemma mbtaGood
      : emptiesStackForever mbtaStack.
      Proof.
        rewrite stackProcess_eta.
        simpl; unfold tickBox, ui.
        apply mbtaGood'.
      Qed.

      Definition mbta := runStackProcess mbtaStack mbtaGood.

    End mbta.
  End components.

  Require Import ExtrOcamlBasic ExtrOcamlString.
  Extraction "ExampleMBTA" mbta.
End MBTARequester.

author: JasonGross

repo: apps

save_path: github-repos/coq/JasonGross-apps


text:
(* "simp" inverts all hypotheses whose inversion results in exactly one subgoal,
   but only those that can be inverted without having to first simplify them to
   see that they're an invertible Inductive, and it also does not destruct records. *)

Require Import Coq.ZArith.ZArith.

Ltac head_of_app e :=
  match e with
  | ?f ?a => head_of_app f
  | _ => e
  end.

Ltac destruct_unique_match :=
  match goal with
  | H: context[match ?e with _ => _ end] |- _ =>
    match goal with
    | |- _ => is_var e; destruct e
    | |- _ => let N := fresh "E" in destruct e eqn: N
    end;
    try (exfalso; (contradiction || discriminate || congruence));
    [> ] (* "(let n := numgoals in guard n = 1)" would not be executed if 0 goals *)
  end.

Definition protected(P: Prop) := P.

Ltac protect_equalities :=
  repeat match goal with
         | H: ?a = ?b |- _ => change (protected (a = b)) in H
         end.

Ltac unprotect_equalities :=
  repeat match goal with
         | H: protected (?a = ?b) |- _ => change (a = b) in H
         end.

Ltac invert_hyp H := protect_equalities; inversion H; clear H; subst; unprotect_equalities.

(* succeeds iff the type of H is an inductive with several constructors *)
Ltac has_several_constructors H :=
  let T := type of H in
  let F := fresh in
  (* note: we do the "clear -H" on the goal "False -> True", so the goal does not contain
     any additional variables that must be kept, which would make "clear" and "case" slow *)
  let r := constr:(ltac:(clear -H; intro F; case H; [ case F | case F | case F .. ])
                   : False -> True) in
  idtac.

(* Given a hypothesis H, returns the induction principle for it *)
Ltac get_ind_principle H :=
  let T := type of H in
  let r := constr:(ltac:(clear -H; induction H; intros; exact I) : T -> True) in
  head_of_app r.

(* Checks if all indices of term t are vars.
   ip should be the induction principle for the type of t, which we use
   to check whether an argument in t is a parameter (then ip can be specialized with it)
   or an index (then it cannot).
   Returns the partially specialized ip if we're still processing parameters, tt if we're
   processing indices and all of them so far were variables, or fails if any non-var indices
   have been encountered. *)
Ltac all_indices_are_vars ip t :=
  lazymatch t with
  | ?f ?a => lazymatch all_indices_are_vars ip f with
             | tt => let __ := lazymatch constr:(Set) with _ => is_var a end in constr:(tt)
             | ?ip' =>
               match constr:(Set) with
               | _ => constr:(ip' a)
               | _ => let __ := lazymatch constr:(Set) with _ => is_var a end in constr:(tt)
               end
             end
  | ?c => let __ := lazymatch constr:(Set) with _ => is_ind c end in constr:(ip)
  end.

(* Checks if the type of hypothesis H is of the form
   "Ind p1 p2 ... pn i1 i2 ... im",
   where Ind is an inductive type (as in, "is_ind Ind" succeeds),
   p1 p2 ... pn are parameters of the inductive and are allowed to have any shape, while
   i1 i2 ... im are indices of the inductive and must be a variable.
   If this test succeeds and Ind has more than one constructor, then we know that
   "inversion H" will generate more than one subgoal. *)
Ltac all_indices_of_hyp_are_var H :=
  let ip := get_ind_principle H in
  let t := type of H in
  match all_indices_are_vars ip t with
  | ?res => idtac (* ignore res as long as it's not a failure *)
  end.

Ltac unique_inversion :=
  match goal with
  | H: ?P |- _ =>
    (let h := head_of_app P in is_ind h);
    protect_equalities;
    lazymatch P with
    | ?LHS = ?RHS =>
      (* don't simpl if user didn't simpl *)
      let h1 := head_of_app LHS in is_constructor h1;
      let h2 := head_of_app RHS in is_constructor h2;
      inversion H; clear H
    | _ * _  => destruct H
    (* Note: the following two cases reuse the name H, so they will only succeed if H was cleared
       (which might not be the case if H is a section variable), and enforcing that H is cleared
       is needed to avoid infinite looping *)
    | _ /\ _ => (* destruct "H: A0 /\ A1 /\ ... An" into "Hp0: A0, Hp1: A1, .. Hpn: An" *)
      let Hl := fresh H "p0" in destruct H as [Hl H];
      lazymatch type of H with
      | _ /\ _ => idtac (* not done yet *)
      | _ => let Hr := fresh H "p0" in rename H into Hr (* done, make naming uniform for last clause *)
      end
    | exists y, _ => let yf := fresh y in destruct H as [yf H]
    | _ => (* By default, we don't want to destruct types with only one constructor
              (in particular, Class and Record are simpler if not destructed).
              The exceptions (ie types with only one constructor which we still want to
              destruct) are treated above). *)
           has_several_constructors H;
           tryif all_indices_of_hyp_are_var H then (
               (* idtac "no need to invert" P; *)
               fail "will definitely get more than one subgoal"
           ) else (
               (* idtac "gonna invert" P; *)
               inversion H; clear H
           )
    end;
    [> (* require exactly one goal *)
     subst;
     unprotect_equalities]
  end.

Ltac simpl_Z_eqb :=
  match goal with
  | H: _ =? _ = true  |- _ => apply Z.eqb_eq in H; subst
  | H: _ =? _ = false |- _ => apply Z.eqb_neq in H
  end.

Ltac simp_step :=
  destruct_unique_match
  || unique_inversion
  || simpl_Z_eqb.

Ltac simp := repeat simp_step.

author: mit-plv

repo: coqutil

save_path: github-repos/coq/mit-plv-coqutil


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

(** Equality on natural numbers *)

Open Local Scope nat_scope.

Implicit Types m n x y : nat.

(** * Propositional equality  *)

Fixpoint eq_nat n m : Prop :=
  match n, m with
    | O, O => True
    | O, S _ => False
    | S _, O => False
    | S n1, S m1 => eq_nat n1 m1
  end.

Theorem eq_nat_refl : forall n, eq_nat n n.
  induction n; simpl in |- *; auto.
Qed.
Hint Resolve eq_nat_refl: arith v62.

(** [eq] restricted to [nat] and [eq_nat] are equivalent *)

Lemma eq_eq_nat : forall n m, n = m -> eq_nat n m.
  induction 1; trivial with arith.
Qed.
Hint Immediate eq_eq_nat: arith v62.

Lemma eq_nat_eq : forall n m, eq_nat n m -> n = m.
  induction n; induction m; simpl in |- *; contradiction || auto with arith.
Qed.
Hint Immediate eq_nat_eq: arith v62.

Theorem eq_nat_is_eq : forall n m, eq_nat n m <-> n = m.
Proof.
  split; auto with arith.
Qed.

Theorem eq_nat_elim :
  forall n (P:nat -> Prop), P n -> forall m, eq_nat n m -> P m.
Proof.
  intros; replace m with n; auto with arith.
Qed.

Theorem eq_nat_decide : forall n m, {eq_nat n m} + {~ eq_nat n m}.
Proof.
  induction n.
  destruct m as [| n].
  auto with arith.
  intros; right; red in |- *; trivial with arith.
  destruct m as [| n0].
  right; red in |- *; auto with arith.
  intros.
  simpl in |- *.
  apply IHn.
Defined.

(** * Boolean equality on [nat] *)

Fixpoint beq_nat n m : bool :=
  match n, m with
    | O, O => true
    | O, S _ => false
    | S _, O => false
    | S n1, S m1 => beq_nat n1 m1
  end.

Lemma beq_nat_refl : forall n, true = beq_nat n n.
Proof.
  intro x; induction x; simpl in |- *; auto.
Qed.

Definition beq_nat_eq : forall x y, true = beq_nat x y -> x = y.
Proof.
  double induction x y; simpl in |- *.
    reflexivity.
    intros n H1 H2. discriminate H2.
    intros n H1 H2. discriminate H2.
    intros n H1 z H2 H3. case (H2 _ H3). reflexivity.
Defined.

Lemma beq_nat_true : forall x y, beq_nat x y = true -> x=y.
Proof.
 induction x; destruct y; simpl; auto; intros; discriminate.
Qed.

Lemma beq_nat_false : forall x y, beq_nat x y = false -> x<>y.
Proof.
 induction x; destruct y; simpl; auto; intros; discriminate.
Qed.

Lemma beq_nat_true_iff : forall x y, beq_nat x y = true <-> x=y.
Proof.
 split. apply beq_nat_true.
 intros; subst; symmetry; apply beq_nat_refl.
Qed.

Lemma beq_nat_false_iff : forall x y, beq_nat x y = false <-> x<>y.
Proof.
 intros x y.
 split. apply beq_nat_false.
 generalize (beq_nat_true_iff x y).
 destruct beq_nat; auto.
 intros IFF NEQ. elim NEQ. apply IFF; auto.
Qed.

repo: Coq-misc


text:
Theorem plus_2_3 : (S(S O)) + (S(S(S O))) = (S(S(S(S(S O))))).
Proof.
  exact (eq_refl 5).
Qed.

Theorem plus_O_n : (forall n, O + n = n).
Proof.
  intros n.
  exact (eq_refl n).
Qed.

repo: Coq-Work