text:
Require Import Effects.
Require Import delay.Eff.

Set Universe Polymorphism.

Fixpoint eval (n:nat) {A} {struct n} : M A -> option A.
Proof.
  intros x. destruct x as [a | x].
  - exact (Some a).
  - destruct n.
    + exact None.
    + exact (eval n _ x).
Defined.

Declare Effect delay.Eff.

(* Effect Definition foo : Type using delay.Eff.  *)

(* Inductive bool : Type :=  true : bool | false : bool. *)

(* Effect Translate unit using delay.Eff. *)

Effect Definition bool : Type using delay.Eff.
Proof.
  refine (ret (exist _ _ (M bool) _)).
  refine (fun b => bind b (fun b => b)).
Defined.

Inductive Paths {A : Type} (x : A) : A -> Type :=  id_path : Paths x x.

(* Effect Translate Paths using delay.Eff. *)

Effect Definition eq : forall (A : Type) (x : A), A -> Type using delay.Eff.
Proof.
  intros A x y.
  refine (ret (exist _ _ (M (Paths x y)) _)).
  refine (fun b => bind b (fun b => b)).
Defined.

Inductive Value {A} : M A -> A -> Type :=
  value_return : forall (a : A), Value (ret a) a
| value_step : forall (x: M A) (a : A), Value x a -> Value (step x) a.

CoInductive Diverge {A} : M A -> Type :=
  diverge : forall (x : M A), Diverge x -> Diverge (step x).

CoInductive included {A} : M A -> M A -> Type :=
  le_value : forall (x y : M A) (a:A) , Value x a -> Value y a -> included x y
| le_steps : forall (x y : M A), included x y -> included (step x) (step y)
| le_lstep : forall (x y : M A), included x y -> included (step x) y.

Infix "⊑" := included (at level 100).

Definition Increasing_sequence A (f : nat -> M A) := forall n, f n ⊑ f (S n).

CoFixpoint fstConv {A} : M A -> M A -> M A :=
  fun x y =>
    match x with
    | ret a => ret a
    | step x_ => match y with
               | ret b => ret b
               | step y_ => step (fstConv x_ y_)
                end
    end.

CoFixpoint searchFstconv_aux {A} : (nat -> M A) -> nat -> M A -> M A :=
  fun f n x => match x with
            ret a => ret a
          | step x => step (searchFstconv_aux f (S n) (fstConv x (f n)))
          end.

CoFixpoint div A : M A := step (div A).

Definition searchFstconv {A} : (nat -> M A) -> M A :=
  fun f => searchFstconv_aux f 0 (div A).

Fixpoint iterate {X} (bot : X) (F : X -> X) (n : nat) : X :=
  match n with
    0 => bot
  | S n => F (iterate bot F n)
  end.

Definition Y2 {A B} (F : (A -> M B) -> A -> M B)  : A -> M B := fun x => searchFstconv (fun n => iterate (fun _ => div _) F n x).

Definition Y {A} (F : M A -> M A) : M A := searchFstconv (fun n => iterate (div _) F n).

Effect Definition Box : Type -> Type using delay.Eff.
Proof.
  intro T.
  refine (ret (exist _ _ (M (El T).(wit)) _)).
  refine (fun b => bind b (fun b => b)).
Defined.

Effect Definition fixp2 : forall (A B : Type), ((A -> B) -> (A -> Box B)) -> (A -> B) using delay.Eff.
Proof.
  intros A B f x. cbn in *.
  destruct B as [B | B] ; simpl in *; try exact tt.
  apply B.(prf). generalize dependent x. refine (Y2 _).
  intros g x. exact (f (fun x => B.(prf) (g x)) x).
Defined.

Effect Definition nat : Type using delay.Eff.
Proof.
  refine (ret (exist _ _ (M nat) _)).
  refine (fun b => bind b (fun b => b)).
Defined.

Effect Definition zero : nat using delay.Eff.
Proof.
  refine (ret 0).
Defined.

Effect Definition suc : nat -> nat using delay.Eff.
Proof.
  refine (map S).
Defined.

Effect Definition nat_rec :  forall A :Type,
       A ->
       (forall n : nat, A -> A) ->
       forall n : nat, A using delay.Eff.
Proof.
  cbn. intros P P0 PS n. refine (hbind n _).
  clear n; intro n. induction n.
  - exact P0.
  - exact (PS (ret n) IHn).
Defined.

Effect Definition unbox : forall (A : Type), Box A -> A using delay.Eff.
Proof.
  intros A. cbn in *.
  destruct A as [A | A]; simpl in *; try exact (fun _ => tt).
  exact A.(prf).
Defined.

Effect Definition box : forall (A : Type), A -> Box A using delay.Eff.
Proof.
  intros A. cbn in *.
  destruct A as [A | A]; simpl in *; try exact (fun _ => ret tt).
  exact ret.
Defined.

Effect Definition base_box : nat -> Box nat using delay.Eff.
Proof.
  refine (map ret).
Defined.

Definition div2_aux : (nat -> nat) -> nat -> Box nat.
Proof.
  intros f m. apply base_box.
  refine (nat_rec _ _ _ m); clear m.
  - exact zero.
  - intros m Hm. refine (nat_rec _ _ _ m); clear m.
    + exact zero.
    + intros m Hm'. exact (suc (f m)).
Defined.

Definition div2 : nat -> nat.
Proof.
  refine (fixp2 _ _ _). refine div2_aux.
Defined.

Effect Translate div2_aux using delay.Eff.

Effect Translate div2 using delay.Eff.

Effect Definition option : Type -> Type using delay.Eff.
Proof.
  refine (fun A => bind A _). clear A; intro A.
  refine (ret (exist _ _ (M (option A.(wit))) _)).
  refine (fun b => bind b (fun b => b)).
Defined.

Effect Definition some : forall A, A -> option A using delay.Eff.
Proof.
  cbn. intros A x. destruct A as [A | A ]; cbn.
  - exact (ret (Some x)).
  - exact tt.
Defined.

Effect Definition evalM : nat -> option nat using delay.Eff.
Proof.
  cbn. intros n.
  refine (ret (option_map ret (eval 1000 n))).
Defined.

Effect Definition eq_div2 : eq _ (evalM (div2 (suc (suc (suc (suc (suc zero))))))) (evalM (suc (suc zero))) using delay.Eff.
Proof.
compute. refine (ret (id_path _)).
Defined.

author: CoqHott

repo: coq-effects

save_path: github-repos/coq/CoqHott-coq-effects


text:
Require Export P08.

(* is_redblack t col n:
t is a red-black tree having n black nodes from any leaf to the root,
and it is legal to put t as a subtree into the child of a new root with color col. *)

Ltac ultimate_tactic :=
      repeat match goal with
      | (* Let's destruct all match's conditions *)
        [ |- context[match ?c with _ => _ end] ] => destruct c

      (* A few rules to find false hypothesis: *)
      | (* is_redblack (T Red _ _ _ (T Red)) _ is impossible. *)
      H: is_redblack (T Red _ _ _ (T Red _ _ _ _)) _ _ |- _ => inv H
      | (* is_redblack (T Red _ _ _ _) Red _ is impossible. *)
      H: is_redblack (T Red _ _ _ _) Red _ |- _ => inv H
      | (*  nearly_redblack E n cannot happen *)
      H: nearly_redblack E _ |- _ => inv H
      | (* is_redblack E _ (S n) cannot happen *)
      H: is_redblack E _ (S _) |- _ => inv H

      (* Then, a few rules for simplification: *)
      | (* If is_redblack E _ n0, n0 is 0 *)
      H: is_redblack E _ ?n0 |- _ => inv H
      | (* If is_redblack _ _ 0, invert it; either it is false or makes splitted hypothesis *)
      H: is_redblack _ _ 0 |- _ => inv H

      (* A few cases where the tree's depth is constant: *)
      | |- nearly_redblack _ 1 => constructor
      | |- is_redblack E _ 0 => apply IsRB_leaf
      | |- is_redblack (T _ _ _ _ _) _ 1 => constructor
      | |- is_redblack _ _ 0 => constructor

      (* Now, observe which goals remain, and add patterns one by one *)
      | |- nearly_redblack (T _ _ _ _ _) (S _) => constructor
      | |- is_redblack (T _ _ _ _ _) _ (S _) => constructor
      | H: is_redblack (T _ _ _ _ _) _ _ |- _ => inv H
      | H: is_redblack ?a Red ?b |- is_redblack ?a Black ?b => apply is_redblack_toblack
      | H1: nearly_redblack (T _ _ _ _ _) _ |- _ => inv H1
      end.

Lemma ins_is_redblack:
  forall x vx s n,
    (is_redblack s Black n -> nearly_redblack (ins x vx s) n) /\
    (is_redblack s Red n -> is_redblack (ins x vx s) Black n).
Proof.
induction s; intro n; simpl; split; intros; inv H; repeat constructor; auto.
destruct (IHs1 n); clear IHs1.
destruct (IHs2 n); clear IHs2.
specialize (H0 H6).
specialize (H2 H7).
clear H H1.
unfold balance.

{
  bdestruct (ltb x k); bdestruct (ltb k x);
  constructor; try assumption; apply is_redblack_toblack; assumption.
}
{
  assert (IHs1' := IHs1 n0). inv IHs1'. clear IHs1.
  assert (IHs2' := IHs2 n0). inv IHs2'. clear IHs2.

  assert (HNR1 := H H7).
  assert (HNR2 := H1 H8).
  bdestruct (ltb x k); bdestruct (ltb k x); try nia; simpl;
    ultimate_tactic; assumption.
}
{
  assert (IHs1' := IHs1 n0). inv IHs1'. clear IHs1.
  assert (IHs2' := IHs2 n0). inv IHs2'. clear IHs2.

  assert (HNR1 := H H7).
  assert (HNR2 := H1 H8).
  bdestruct (ltb x k); bdestruct (ltb k x); try nia; simpl;
    ultimate_tactic; assumption.
}
Qed.

author: snu-sf-class


text:
(** Generated by coq-of-ocaml *)
Require Import OCaml.OCaml.

Local Set Primitive Projections.
Local Open Scope string_scope.
Local Open Scope Z_scope.
Local Open Scope type_scope.
Import ListNotations.

Unset Positivity Checking.
Unset Guard Checking.

Inductive nat : Set :=
| O : nat
| S : nat -> nat.

Inductive natural : Set :=
| Zero : natural
| Succ : natural -> natural.

Fixpoint plus (plus_arg0 : natural) (plus_arg1 : natural) {struct plus_arg0}
  : natural :=
  match plus_arg0 with
  | Zero => plus_arg1
  | Succ n => Succ (plus n plus_arg1)
  end.

Fixpoint mult (mult_arg0 : natural) (mult_arg1 : natural) {struct mult_arg0}
  : natural :=
  match mult_arg0 with
  | Zero => Zero
  | Succ n => plus (mult n mult_arg1) mult_arg1
  end.

Definition synth (lf2 : natural) (z : natural) : natural := plus z lf2.

author: yalhessi

repo: lemmaranker

save_path: github-repos/coq/yalhessi-lemmaranker


text:
(**************************************************************************
* Product of Data Structures                                              *
**************************************************************************)

Set Implicit Arguments.
From TLC Require Import LibTactics LibLogic LibReflect.

(* ********************************************************************** *)
(** * Unit type *)

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

(** From the Prelude.

  Inductive unit : Type :=
    | tt : unit.

  Add Printing If bool.
  Delimit Scope bool_scope with bool.

*)

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

#[global]
Instance Inhab_unit : Inhab unit.
Proof using. intros. apply (Inhab_of_val tt). Qed.

(* ********************************************************************** *)
(** * Properties *)

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

Lemma unit_eq : forall (tt1 tt2 : unit),
  tt1 = tt2.
Proof using. intros. destruct tt1. destruct~ tt2. Qed.

author: charguer

repo: tlc

save_path: github-repos/coq/charguer-tlc


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        *)
(************************************************************************)

Require Import RIneq.
Require Import Omega.
Open Local Scope R_scope.

Lemma Rlt_R0_R2 : 0 < 2.
change 2 with (INR 2); apply lt_INR_0; apply lt_O_Sn.
Qed.

Notation Rplus_lt_pos := Rplus_lt_0_compat (only parsing).

Lemma IZR_eq : forall z1 z2:Z, z1 = z2 -> IZR z1 = IZR z2.
intros; rewrite H; reflexivity.
Qed.

Lemma IZR_neq : forall z1 z2:Z, z1 <> z2 -> IZR z1 <> IZR z2.
intros; red in |- *; intro; elim H; apply eq_IZR; assumption.
Qed.

Ltac discrR :=
  try
   match goal with
   |  |- (?X1 <> ?X2) =>
       change 2 with (IZR 2);
       change 1 with (IZR 1);
       change 0 with (IZR 0);
       repeat
         rewrite <- plus_IZR ||
           rewrite <- mult_IZR ||
           rewrite <- Ropp_Ropp_IZR || rewrite Z_R_minus;
       apply IZR_neq; try discriminate
   end.

Ltac prove_sup0 :=
  match goal with
  |  |- (0 < 1) => apply Rlt_0_1
  |  |- (0 < ?X1) =>
      repeat
       (apply Rmult_lt_0_compat || apply Rplus_lt_pos;
         try apply Rlt_0_1 || apply Rlt_R0_R2)
  |  |- (?X1 > 0) => change (0 < X1) in |- *; prove_sup0
  end.

Ltac omega_sup :=
  change 2 with (IZR 2);
  change 1 with (IZR 1);
  change 0 with (IZR 0);
  repeat
    rewrite <- plus_IZR ||
      rewrite <- mult_IZR || rewrite <- Ropp_Ropp_IZR || rewrite Z_R_minus;
  apply IZR_lt; omega.

Ltac prove_sup :=
  match goal with
  |  |- (?X1 > ?X2) => change (X2 < X1) in |- *; prove_sup
  |  |- (0 < ?X1) => prove_sup0
  |  |- (- ?X1 < 0) => rewrite <- Ropp_0; prove_sup
  |  |- (- ?X1 < - ?X2) => apply Ropp_lt_gt_contravar; prove_sup
  |  |- (- ?X1 < ?X2) => apply Rlt_trans with 0; prove_sup
  |  |- (?X1 < ?X2) => omega_sup
  | _ => idtac
  end.

Ltac Rcompute :=
  change 2 with (IZR 2);
  change 1 with (IZR 1);
  change 0 with (IZR 0);
  repeat
    rewrite <- plus_IZR ||
      rewrite <- mult_IZR || rewrite <- Ropp_Ropp_IZR || rewrite Z_R_minus;
  apply IZR_eq; try reflexivity.

repo: Coq-misc


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

(** Correctness proof for operator strength reduction. *)

Require Import Coqlib Compopts.
Require Import Integers Floats Values Memory Globalenvs Events.
Require Import Op Registers RTL ValueDomain.
Require Import ConstpropOp.

Section STRENGTH_REDUCTION.
Context `{memory_model_prf: Mem.MemoryModel}.

Variable bc: block_classification.
Variable ge: genv.
Hypothesis GENV: genv_match bc ge.
Variable sp: block.
Hypothesis STACK: bc sp = BCstack.
Variable ae: AE.t.
Variable e: regset.
Variable m: mem.
Hypothesis MATCH: ematch bc e ae.

Lemma match_G:
  forall r id ofs,
  AE.get r ae = Ptr(Gl id ofs) -> Val.lessdef e#r (Genv.symbol_address ge id ofs).
Proof.
  intros. apply vmatch_ptr_gl with bc; auto. rewrite <- H. apply MATCH.
Qed.

Lemma match_S:
  forall r ofs,
  AE.get r ae = Ptr(Stk ofs) -> Val.lessdef e#r (Vptr sp ofs).
Proof.
  intros. apply vmatch_ptr_stk with bc; auto. rewrite <- H. apply MATCH.
Qed.

Ltac InvApproxRegs :=
  match goal with
  | [ H: _ :: _ = _ :: _ |- _ ] =>
        injection H; clear H; intros; InvApproxRegs
  | [ H: ?v = AE.get ?r ae |- _ ] =>
        generalize (MATCH r); rewrite <- H; clear H; intro; InvApproxRegs
  | _ => idtac
  end.

Ltac SimplVM :=
  match goal with
  | [ H: vmatch _ ?v (I ?n) |- _ ] =>
      let E := fresh in
      assert (E: v = Vint n) by (inversion H; auto);
      rewrite E in *; clear H; SimplVM
  | [ H: vmatch _ ?v (L ?n) |- _ ] =>
      let E := fresh in
      assert (E: v = Vlong n) by (inversion H; auto);
      rewrite E in *; clear H; SimplVM
  | [ H: vmatch _ ?v (F ?n) |- _ ] =>
      let E := fresh in
      assert (E: v = Vfloat n) by (inversion H; auto);
      rewrite E in *; clear H; SimplVM
  | [ H: vmatch _ ?v (FS ?n) |- _ ] =>
      let E := fresh in
      assert (E: v = Vsingle n) by (inversion H; auto);
      rewrite E in *; clear H; SimplVM
  | [ H: vmatch _ ?v (Ptr(Gl ?id ?ofs)) |- _ ] =>
      let E := fresh in
      assert (E: Val.lessdef v (Genv.symbol_address ge id ofs)) by (eapply vmatch_ptr_gl; eauto);
      clear H; SimplVM
  | [ H: vmatch _ ?v (Ptr(Stk ?ofs)) |- _ ] =>
      let E := fresh in
      assert (E: Val.lessdef v (Vptr sp ofs)) by (eapply vmatch_ptr_stk; eauto);
      clear H; SimplVM
  | _ => idtac
  end.

Lemma eval_Olea_ptr:
  forall a el,
  eval_operation ge (Vptr sp Ptrofs.zero) (Olea_ptr a) el m = eval_addressing ge (Vptr sp Ptrofs.zero) a el.
Proof.
  unfold Olea_ptr, eval_addressing; intros. destruct Archi.ptr64; auto.
Qed.

Lemma const_for_result_correct:
  forall a op v,
  const_for_result a = Some op ->
  vmatch bc v a ->
  exists v', eval_operation ge (Vptr sp Ptrofs.zero) op nil m = Some v' /\ Val.lessdef v v'.
Proof.
  unfold const_for_result. generalize Archi.ptr64; intros ptr64; intros.
  destruct a; inv H; SimplVM.
- (* integer *)
  exists (Vint n); auto.
- (* long *)
  destruct ptr64; inv H2. exists (Vlong n); auto.
- (* float *)
  destruct (Compopts.generate_float_constants tt); inv H2. exists (Vfloat f); auto.
- (* single *)
  destruct (Compopts.generate_float_constants tt); inv H2. exists (Vsingle f); auto.
- (* pointer *)
  destruct p; try discriminate; SimplVM.
  + (* global *)
    destruct (symbol_is_external id).
  * revert H2; predSpec Ptrofs.eq Ptrofs.eq_spec ofs Ptrofs.zero; intros EQ; inv EQ.
    exists (Genv.symbol_address ge id Ptrofs.zero); auto.
  * inv H2. exists (Genv.symbol_address ge id ofs); split.
    rewrite eval_Olea_ptr. apply eval_addressing_Aglobal.
    auto.
  + (* stack *)
    inv H2. exists (Vptr sp ofs); split.
    rewrite eval_Olea_ptr. rewrite eval_addressing_Ainstack.
    simpl. rewrite Ptrofs.add_zero_l; auto.
    auto.
Qed.

Lemma cond_strength_reduction_correct:
  forall cond args vl,
  vl = map (fun r => AE.get r ae) args ->
  let (cond', args') := cond_strength_reduction cond args vl in
  eval_condition cond' e##args' m = eval_condition cond e##args m.
Proof.
  intros until vl. unfold cond_strength_reduction.
  case (cond_strength_reduction_match cond args vl); simpl; intros; InvApproxRegs; SimplVM.
- apply Val.swap_cmp_bool.
- auto.
- apply Val.swap_cmpu_bool.
- auto.
- apply Val.swap_cmpl_bool.
- auto.
- apply Val.swap_cmplu_bool.
- auto.
- auto.
Qed.

Lemma addr_strength_reduction_32_generic_correct:
  forall addr args vl res,
  vl = map (fun r => AE.get r ae) args ->
  eval_addressing32 ge (Vptr sp Ptrofs.zero) addr e##args = Some res ->
  let (addr', args') := addr_strength_reduction_32_generic addr args vl in
  exists res', eval_addressing32 ge (Vptr sp Ptrofs.zero) addr' e##args' = Some res' /\ Val.lessdef res res'.
Proof.
Local Opaque Val.add.
  assert (A: forall x y, Int.repr (Int.signed x + y) = Int.add x (Int.repr y)).
  { intros; apply Int.eqm_samerepr; auto using Int.eqm_signed_unsigned with ints. }
  assert (B: forall x y z, Int.repr (Int.signed x * y + z) = Int.add (Int.mul x (Int.repr y)) (Int.repr z)).
  { intros; apply Int.eqm_samerepr; apply Int.eqm_add; auto with ints.
    unfold Int.mul; auto using Int.eqm_signed_unsigned with ints. }
  intros until res; intros VL EA.
  unfold addr_strength_reduction_32_generic; destruct (addr_strength_reduction_32_generic_match addr args vl);
  simpl in *; InvApproxRegs; SimplVM; try (inv EA).
- econstructor; split; eauto. rewrite A, Val.add_assoc, Val.add_permut. auto.
- econstructor; split; eauto. rewrite A, Val.add_assoc. auto.
- Local Transparent Val.add.
  econstructor; split; eauto. simpl. rewrite B. auto.
- econstructor; split; eauto. rewrite A, Val.add_permut. auto.
- exists res; auto.
Qed.

Lemma addr_strength_reduction_32_correct:
  forall addr args vl res,
  vl = map (fun r => AE.get r ae) args ->
  eval_addressing32 ge (Vptr sp Ptrofs.zero) addr e##args = Some res ->
  let (addr', args') := addr_strength_reduction_32 addr args vl in
  exists res', eval_addressing32 ge (Vptr sp Ptrofs.zero) addr' e##args' = Some res' /\ Val.lessdef res res'.
Proof.
  intros until res; intros VL EA. unfold addr_strength_reduction_32.
  destruct Archi.ptr64 eqn:SF. apply addr_strength_reduction_32_generic_correct; auto.
  assert (A: forall n, Ptrofs.of_int (Int.repr n) = Ptrofs.repr n) by auto with ptrofs.
  assert (B: forall symb ofs n,
             Genv.symbol_address ge symb (Ptrofs.add ofs (Ptrofs.repr n)) =
             Val.add (Genv.symbol_address ge symb ofs) (Vint (Int.repr n))).
  { intros. rewrite <- A. apply Genv.shift_symbol_address_32; auto. }
Local Opaque Val.add.
  destruct (addr_strength_reduction_32_match addr args vl);
  simpl in *; InvApproxRegs; SimplVM; FuncInv; subst; rewrite ?SF.
- econstructor; split; eauto. rewrite B. apply Val.add_lessdef; auto.
- econstructor; split; eauto. rewrite Ptrofs.add_zero_l.
Local Transparent Val.add.
  inv H0; auto. rewrite H2. simpl; rewrite SF, A. auto.
- econstructor; split; eauto.
  unfold Ptrofs.add at 2. rewrite B.
  fold (Ptrofs.add n1 (Ptrofs.of_int n2)).
  rewrite Genv.shift_symbol_address_32 by auto.
  rewrite ! Val.add_assoc. apply Val.add_lessdef; auto.
- econstructor; split; eauto.
  unfold Ptrofs.add at 2. rewrite B.
  fold (Ptrofs.add n2 (Ptrofs.of_int n1)).
  rewrite Genv.shift_symbol_address_32 by auto.
  rewrite ! Val.add_assoc. rewrite Val.add_permut. apply Val.add_lessdef; auto.
- econstructor; split; eauto. rewrite Ptrofs.add_zero_l. rewrite Val.add_assoc.
  eapply Val.lessdef_trans. apply Val.add_lessdef; eauto.
  simpl. rewrite SF. rewrite Ptrofs.add_assoc. apply Val.lessdef_same; do 3 f_equal. auto with ptrofs.
- econstructor; split; eauto. rewrite Ptrofs.add_zero_l. rewrite Val.add_assoc, Val.add_permut.
  eapply Val.lessdef_trans. apply Val.add_lessdef; eauto.
  simpl. rewrite SF. rewrite <- (Ptrofs.add_commut n2). rewrite Ptrofs.add_assoc.
  apply Val.lessdef_same; do 3 f_equal. auto with ptrofs.
- econstructor; split; eauto. rewrite B. rewrite ! Val.add_assoc. rewrite (Val.add_commut (Vint (Int.repr ofs))).
  apply Val.add_lessdef; auto.
- econstructor; split; eauto. rewrite B. rewrite (Val.add_commut e#r1). rewrite ! Val.add_assoc.
  rewrite (Val.add_commut (Vint (Int.repr ofs))). apply Val.add_lessdef; auto.
- econstructor; split; eauto. rewrite B. rewrite Genv.shift_symbol_address_32 by auto.
  rewrite ! Val.add_assoc. apply Val.add_lessdef; auto.
- econstructor; split; eauto. rewrite B. rewrite ! Val.add_assoc.
  rewrite (Val.add_commut (Vint (Int.repr ofs))). apply Val.add_lessdef; auto.
- econstructor; split; eauto.
  rewrite Genv.shift_symbol_address_32 by auto. auto.
- econstructor; split; eauto.
  rewrite Genv.shift_symbol_address_32 by auto. auto.
- apply addr_strength_reduction_32_generic_correct; auto.
Qed.

Lemma addr_strength_reduction_64_generic_correct:
  forall addr args vl res,
  vl = map (fun r => AE.get r ae) args ->
  eval_addressing64 ge (Vptr sp Ptrofs.zero) addr e##args = Some res ->
  let (addr', args') := addr_strength_reduction_64_generic addr args vl in
  exists res', eval_addressing64 ge (Vptr sp Ptrofs.zero) addr' e##args' = Some res' /\ Val.lessdef res res'.
Proof.
Local Opaque Val.addl.
  assert (A: forall x y, Int64.repr (Int64.signed x + y) = Int64.add x (Int64.repr y)).
  { intros; apply Int64.eqm_samerepr; auto using Int64.eqm_signed_unsigned with ints. }
  assert (B: forall x y z, Int64.repr (Int64.signed x * y + z) = Int64.add (Int64.mul x (Int64.repr y)) (Int64.repr z)).
  { intros; apply Int64.eqm_samerepr; apply Int64.eqm_add; auto with ints.
    unfold Int64.mul; auto using Int64.eqm_signed_unsigned with ints. }
  intros until res; intros VL EA.
  unfold addr_strength_reduction_64_generic; destruct (addr_strength_reduction_64_generic_match addr args vl);
  simpl in *; InvApproxRegs; SimplVM; try (inv EA).
- econstructor; split; eauto. rewrite A, Val.addl_assoc, Val.addl_permut. auto.
- econstructor; split; eauto. rewrite A, Val.addl_assoc. auto.
- Local Transparent Val.addl.
  econstructor; split; eauto. simpl. rewrite B. auto.
- econstructor; split; eauto. rewrite A, Val.addl_permut. auto.
- exists res; auto.
Qed.

Lemma addr_strength_reduction_64_correct:
  forall addr args vl res,
  vl = map (fun r => AE.get r ae) args ->
  eval_addressing64 ge (Vptr sp Ptrofs.zero) addr e##args = Some res ->
  let (addr', args') := addr_strength_reduction_64 addr args vl in
  exists res', eval_addressing64 ge (Vptr sp Ptrofs.zero) addr' e##args' = Some res' /\ Val.lessdef res res'.
Proof.
  intros until res; intros VL EA. unfold addr_strength_reduction_64.
  destruct (negb Archi.ptr64) eqn:SF. apply addr_strength_reduction_64_generic_correct; auto.
  rewrite negb_false_iff in SF.
  assert (A: forall n, Ptrofs.of_int64 (Int64.repr n) = Ptrofs.repr n) by auto with ptrofs.
  assert (B: forall symb ofs n,
             Genv.symbol_address ge symb (Ptrofs.add ofs (Ptrofs.repr n)) =
             Val.addl (Genv.symbol_address ge symb ofs) (Vlong (Int64.repr n))).
  { intros. rewrite <- A. apply Genv.shift_symbol_address_64; auto. }
Local Opaque Val.addl.
  destruct (addr_strength_reduction_64_match addr args vl);
  simpl in *; InvApproxRegs; SimplVM; FuncInv; subst; rewrite ?SF.
- econstructor; split; eauto. rewrite B. apply Val.addl_lessdef; auto.
- econstructor; split; eauto. rewrite Ptrofs.add_zero_l.
Local Transparent Val.addl.
  inv H0; auto. rewrite H2. simpl; rewrite SF, A. auto.
- econstructor; split; eauto.
  unfold Ptrofs.add at 2. rewrite B.
  fold (Ptrofs.add n1 (Ptrofs.of_int64 n2)).
  rewrite Genv.shift_symbol_address_64 by auto.
  rewrite ! Val.addl_assoc. apply Val.addl_lessdef; auto.
- econstructor; split; eauto.
  unfold Ptrofs.add at 2. rewrite B.
  fold (Ptrofs.add n2 (Ptrofs.of_int64 n1)).
  rewrite Genv.shift_symbol_address_64 by auto.
  rewrite ! Val.addl_assoc. rewrite Val.addl_permut. apply Val.addl_lessdef; auto.
- econstructor; split; eauto. rewrite Ptrofs.add_zero_l. rewrite Val.addl_assoc.
  eapply Val.lessdef_trans. apply Val.addl_lessdef; eauto.
  simpl. rewrite SF. rewrite Ptrofs.add_assoc. apply Val.lessdef_same; do 3 f_equal. auto with ptrofs.
- econstructor; split; eauto. rewrite Ptrofs.add_zero_l. rewrite Val.addl_assoc, Val.addl_permut.
  eapply Val.lessdef_trans. apply Val.addl_lessdef; eauto.
  simpl. rewrite SF. rewrite <- (Ptrofs.add_commut n2). rewrite Ptrofs.add_assoc.
  apply Val.lessdef_same; do 3 f_equal. auto with ptrofs.
- econstructor; split; eauto. rewrite B. rewrite Genv.shift_symbol_address_64 by auto.
  rewrite ! Val.addl_assoc. apply Val.addl_lessdef; auto.
- apply addr_strength_reduction_64_generic_correct; auto.
Qed.

Lemma addr_strength_reduction_correct:
  forall addr args vl res,
  vl = map (fun r => AE.get r ae) args ->
  eval_addressing ge (Vptr sp Ptrofs.zero) addr e##args = Some res ->
  let (addr', args') := addr_strength_reduction addr args vl in
  exists res', eval_addressing ge (Vptr sp Ptrofs.zero) addr' e##args' = Some res' /\ Val.lessdef res res'.
Proof.
  unfold eval_addressing, addr_strength_reduction. destruct Archi.ptr64.
- intros until res. destruct (addressing_valid (fst (addr_strength_reduction_64 addr args vl))).
  apply addr_strength_reduction_64_correct.
  intros; exists res; auto.
- apply addr_strength_reduction_32_correct.
Qed.

Lemma make_cmp_base_correct:
  forall c args vl,
  vl = map (fun r => AE.get r ae) args ->
  let (op', args') := make_cmp_base c args vl in
  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op' e##args' m = Some v
         /\ Val.lessdef (Val.of_optbool (eval_condition c e##args m)) v.
Proof.
  intros. unfold make_cmp_base.
  generalize (cond_strength_reduction_correct c args vl H).
  destruct (cond_strength_reduction c args vl) as [c' args']. intros EQ.
  econstructor; split. simpl; eauto. rewrite EQ. auto.
Qed.

Lemma make_cmp_correct:
  forall c args vl,
  vl = map (fun r => AE.get r ae) args ->
  let (op', args') := make_cmp c args vl in
  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op' e##args' m = Some v
         /\ Val.lessdef (Val.of_optbool (eval_condition c e##args m)) v.
Proof.
  intros c args vl.
  assert (Y: forall r, vincl (AE.get r ae) (Uns Ptop 1) = true ->
             e#r = Vundef \/ e#r = Vint Int.zero \/ e#r = Vint Int.one).
  { intros. apply vmatch_Uns_1 with bc Ptop. eapply vmatch_ge. eapply vincl_ge; eauto. apply MATCH. }
  unfold make_cmp. case (make_cmp_match c args vl); intros.
- destruct (Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1)) eqn:E1.
  simpl in H; inv H. InvBooleans. subst n.
  exists (e#r1); split; auto. simpl.
  exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
  destruct (Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1)) eqn:E0.
  simpl in H; inv H. InvBooleans. subst n.
  exists (Val.xor e#r1 (Vint Int.one)); split; auto. simpl.
  exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
  apply make_cmp_base_correct; auto.
- destruct (Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1)) eqn:E0.
  simpl in H; inv H. InvBooleans. subst n.
  exists (e#r1); split; auto. simpl.
  exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
  destruct (Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1)) eqn:E1.
  simpl in H; inv H. InvBooleans. subst n.
  exists (Val.xor e#r1 (Vint Int.one)); split; auto. simpl.
  exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
  apply make_cmp_base_correct; auto.
- apply make_cmp_base_correct; auto.
Qed.

Lemma make_addimm_correct:
  forall n r,
  let (op, args) := make_addimm n r in
  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some v /\ Val.lessdef (Val.add e#r (Vint n)) v.
Proof.
  intros. unfold make_addimm.
  predSpec Int.eq Int.eq_spec n Int.zero; intros.
  subst. exists (e#r); split; auto.
  destruct (e#r); simpl; auto; rewrite ?Int.add_zero, ?Ptrofs.add_zero; auto.
  exists (Val.add e#r (Vint n)); split; auto. simpl. rewrite Int.repr_signed; auto.
Qed.

Lemma make_shlimm_correct:
  forall n r1 r2,
  e#r2 = Vint n ->
  let (op, args) := make_shlimm n r1 r2 in
  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some v /\ Val.lessdef (Val.shl e#r1 (Vint n)) v.
Proof.
  intros; unfold make_shlimm.
  predSpec Int.eq Int.eq_spec n Int.zero; intros. subst.
  exists (e#r1); split; auto. destruct (e#r1); simpl; auto. rewrite Int.shl_zero. auto.
  destruct (Int.ltu n Int.iwordsize).
  econstructor; split. simpl. eauto. auto.
  econstructor; split. simpl. eauto. rewrite H; auto.
Qed.

Lemma make_shrimm_correct:
  forall n r1 r2,
  e#r2 = Vint n ->
  let (op, args) := make_shrimm n r1 r2 in
  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some v /\ Val.lessdef (Val.shr e#r1 (Vint n)) v.
Proof.
  intros; unfold make_shrimm.
  predSpec Int.eq Int.eq_spec n Int.zero; intros. subst.
  exists (e#r1); split; auto. destruct (e#r1); simpl; auto. rewrite Int.shr_zero. auto.
  destruct (Int.ltu n Int.iwordsize).
  econstructor; split. simpl. eauto. auto.
  econstructor; split. simpl. eauto. rewrite H; auto.
Qed.

Lemma make_shruimm_correct:
  forall n r1 r2,
  e#r2 = Vint n ->
  let (op, args) := make_shruimm n r1 r2 in
  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some v /\ Val.lessdef (Val.shru e#r1 (Vint n)) v.
Proof.
  intros; unfold make_shruimm.
  predSpec Int.eq Int.eq_spec n Int.zero; intros. subst.
  exists (e#r1); split; auto. destruct (e#r1); simpl; auto. rewrite Int.shru_zero. auto.
  destruct (Int.ltu n Int.iwordsize).
  econstructor; split. simpl. eauto. auto.
  econstructor; split. simpl. eauto. rewrite H; auto.
Qed.

Lemma make_mulimm_correct:
  forall n r1,
  let (op, args) := make_mulimm n r1 in
  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some v /\ Val.lessdef (Val.mul e#r1 (Vint n)) v.
Proof.
  intros; unfold make_mulimm.
  predSpec Int.eq Int.eq_spec n Int.zero; intros. subst.
  exists (Vint Int.zero); split; auto. destruct (e#r1); simpl; auto. rewrite Int.mul_zero; auto.
  predSpec Int.eq Int.eq_spec n Int.one; intros. subst.
  exists (e#r1); split; auto. destruct (e#r1); simpl; auto. rewrite Int.mul_one; auto.
  destruct (Int.is_power2 n) eqn:?; intros.
  rewrite (Val.mul_pow2 e#r1 _ _ Heqo). econstructor; split. simpl; eauto. auto.
  econstructor; split; eauto. auto.
Qed.

Lemma make_divimm_correct:
  forall n r1 r2 v,
  Val.divs e#r1 e#r2 = Some v ->
  e#r2 = Vint n ->
  let (op, args) := make_divimm n r1 r2 in
  exists w, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some w /\ Val.lessdef v w.
Proof.
  intros; unfold make_divimm.
  destruct (Int.is_power2 n) eqn:?.
  destruct (Int.ltu i (Int.repr 31)) eqn:?.
  exists v; split; auto. simpl. eapply Val.divs_pow2; eauto. congruence.
  exists v; auto.
  exists v; auto.
Qed.

Lemma make_divuimm_correct:
  forall n r1 r2 v,
  Val.divu e#r1 e#r2 = Some v ->
  e#r2 = Vint n ->
  let (op, args) := make_divuimm n r1 r2 in
  exists w, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some w /\ Val.lessdef v w.
Proof.
  intros; unfold make_divuimm.
  destruct (Int.is_power2 n) eqn:?.
  econstructor; split. simpl; eauto.
  rewrite H0 in H. erewrite Val.divu_pow2 by eauto. auto.
  exists v; auto.
Qed.

Lemma make_moduimm_correct:
  forall n r1 r2 v,
  Val.modu e#r1 e#r2 = Some v ->
  e#r2 = Vint n ->
  let (op, args) := make_moduimm n r1 r2 in
  exists w, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some w /\ Val.lessdef v w.
Proof.
  intros; unfold make_moduimm.
  destruct (Int.is_power2 n) eqn:?.
  exists v; split; auto. simpl. decEq. eapply Val.modu_pow2; eauto. congruence.
  exists v; auto.
Qed.

Lemma make_andimm_correct:
  forall n r x,
  vmatch bc e#r x ->
  let (op, args) := make_andimm n r x in
  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some v /\ Val.lessdef (Val.and e#r (Vint n)) v.
Proof.
  intros; unfold make_andimm.
  predSpec Int.eq Int.eq_spec n Int.zero; intros.
  subst n. exists (Vint Int.zero); split; auto. destruct (e#r); simpl; auto. rewrite Int.and_zero; auto.
  predSpec Int.eq Int.eq_spec n Int.mone; intros.
  subst n. exists (e#r); split; auto. destruct (e#r); simpl; auto. rewrite Int.and_mone; auto.
  destruct (match x with Uns _ k => Int.eq (Int.zero_ext k (Int.not n)) Int.zero
                       | _ => false end) eqn:UNS.
  destruct x; try congruence.
  exists (e#r); split; auto.
  inv H; auto. simpl. replace (Int.and i n) with i; auto.
  generalize (Int.eq_spec (Int.zero_ext n0 (Int.not n)) Int.zero); rewrite UNS; intro EQ.
  Int.bit_solve. destruct (zlt i0 n0).
  replace (Int.testbit n i0) with (negb (Int.testbit Int.zero i0)).
  rewrite Int.bits_zero. simpl. rewrite andb_true_r. auto.
  rewrite <- EQ. rewrite Int.bits_zero_ext by omega. rewrite zlt_true by auto.
  rewrite Int.bits_not by auto. apply negb_involutive.
  rewrite H6 by auto. auto.
  econstructor; split; eauto. auto.
Qed.

Lemma make_orimm_correct:
  forall n r,
  let (op, args) := make_orimm n r in
  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some v /\ Val.lessdef (Val.or e#r (Vint n)) v.
Proof.
  intros; unfold make_orimm.
  predSpec Int.eq Int.eq_spec n Int.zero; intros.
  subst n. exists (e#r); split; auto. destruct (e#r); simpl; auto. rewrite Int.or_zero; auto.
  predSpec Int.eq Int.eq_spec n Int.mone; intros.
  subst n. exists (Vint Int.mone); split; auto. destruct (e#r); simpl; auto. rewrite Int.or_mone; auto.
  econstructor; split; eauto. auto.
Qed.

Lemma make_xorimm_correct:
  forall n r,
  let (op, args) := make_xorimm n r in
  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some v /\ Val.lessdef (Val.xor e#r (Vint n)) v.
Proof.
  intros; unfold make_xorimm.
  predSpec Int.eq Int.eq_spec n Int.zero; intros.
  subst n. exists (e#r); split; auto. destruct (e#r); simpl; auto. rewrite Int.xor_zero; auto.
  predSpec Int.eq Int.eq_spec n Int.mone; intros.
  subst n. exists (Val.notint e#r); split; auto.
  econstructor; split; eauto. auto.
Qed.

Lemma make_addlimm_correct:
  forall n r,
  let (op, args) := make_addlimm n r in
  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some v /\ Val.lessdef (Val.addl e#r (Vlong n)) v.
Proof.
  intros. unfold make_addlimm.
  predSpec Int64.eq Int64.eq_spec n Int64.zero; intros.
  subst. exists (e#r); split; auto.
  destruct (e#r); simpl; auto; rewrite ? Int64.add_zero, ? Ptrofs.add_zero; auto.
  exists (Val.addl e#r (Vlong n)); split; auto. simpl. rewrite Int64.repr_signed; auto.
Qed.

Lemma make_shllimm_correct:
  forall n r1 r2,
  e#r2 = Vint n ->
  let (op, args) := make_shllimm n r1 r2 in
  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some v /\ Val.lessdef (Val.shll e#r1 (Vint n)) v.
Proof.
  intros; unfold make_shllimm.
  predSpec Int.eq Int.eq_spec n Int.zero; intros. subst.
  exists (e#r1); split; auto. destruct (e#r1); simpl; auto.
  unfold Int64.shl'. rewrite Z.shiftl_0_r, Int64.repr_unsigned. auto.
  destruct (Int.ltu n Int64.iwordsize').
  econstructor; split. simpl. eauto. auto.
  econstructor; split. simpl. eauto. rewrite H; auto.
Qed.

Lemma make_shrlimm_correct:
  forall n r1 r2,
  e#r2 = Vint n ->
  let (op, args) := make_shrlimm n r1 r2 in
  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some v /\ Val.lessdef (Val.shrl e#r1 (Vint n)) v.
Proof.
  intros; unfold make_shrlimm.
  predSpec Int.eq Int.eq_spec n Int.zero; intros. subst.
  exists (e#r1); split; auto. destruct (e#r1); simpl; auto.
  unfold Int64.shr'. rewrite Z.shiftr_0_r, Int64.repr_signed. auto.
  destruct (Int.ltu n Int64.iwordsize').
  econstructor; split. simpl. eauto. auto.
  econstructor; split. simpl. eauto. rewrite H; auto.
Qed.

Lemma make_shrluimm_correct:
  forall n r1 r2,
  e#r2 = Vint n ->
  let (op, args) := make_shrluimm n r1 r2 in
  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some v /\ Val.lessdef (Val.shrlu e#r1 (Vint n)) v.
Proof.
  intros; unfold make_shrluimm.
  predSpec Int.eq Int.eq_spec n Int.zero; intros. subst.
  exists (e#r1); split; auto. destruct (e#r1); simpl; auto.
  unfold Int64.shru'. rewrite Z.shiftr_0_r, Int64.repr_unsigned. auto.
  destruct (Int.ltu n Int64.iwordsize').
  econstructor; split. simpl. eauto. auto.
  econstructor; split. simpl. eauto. rewrite H; auto.
Qed.

Lemma make_mullimm_correct:
  forall n r1,
  let (op, args) := make_mullimm n r1 in
  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some v /\ Val.lessdef (Val.mull e#r1 (Vlong n)) v.
Proof.
  intros; unfold make_mullimm.
  predSpec Int64.eq Int64.eq_spec n Int64.zero; intros. subst.
  exists (Vlong Int64.zero); split; auto. destruct (e#r1); simpl; auto. rewrite Int64.mul_zero; auto.
  predSpec Int64.eq Int64.eq_spec n Int64.one; intros. subst.
  exists (e#r1); split; auto. destruct (e#r1); simpl; auto. rewrite Int64.mul_one; auto.
  destruct (Int64.is_power2' n) eqn:?; intros.
  exists (Val.shll e#r1 (Vint i)); split; auto.
  destruct (e#r1); simpl; auto.
  erewrite Int64.is_power2'_range by eauto.
  erewrite Int64.mul_pow2' by eauto. auto.
  econstructor; split; eauto. auto.
Qed.

Lemma make_divlimm_correct:
  forall n r1 r2 v,
  Val.divls e#r1 e#r2 = Some v ->
  e#r2 = Vlong n ->
  let (op, args) := make_divlimm n r1 r2 in
  exists w, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some w /\ Val.lessdef v w.
Proof.
  intros; unfold make_divlimm.
  destruct (Int64.is_power2' n) eqn:?. destruct (Int.ltu i (Int.repr 63)) eqn:?.
  rewrite H0 in H. econstructor; split. simpl; eauto. eapply Val.divls_pow2; eauto. auto.
  exists v; auto.
  exists v; auto.
Qed.

Lemma make_divluimm_correct:
  forall n r1 r2 v,
  Val.divlu e#r1 e#r2 = Some v ->
  e#r2 = Vlong n ->
  let (op, args) := make_divluimm n r1 r2 in
  exists w, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some w /\ Val.lessdef v w.
Proof.
  intros; unfold make_divluimm.
  destruct (Int64.is_power2' n) eqn:?.
  econstructor; split. simpl; eauto.
  rewrite H0 in H. destruct (e#r1); inv H. destruct (Int64.eq n Int64.zero); inv H2.
  simpl.
  erewrite Int64.is_power2'_range by eauto.
  erewrite Int64.divu_pow2' by eauto.  auto.
  exists v; auto.
Qed.

Lemma make_modluimm_correct:
  forall n r1 r2 v,
  Val.modlu e#r1 e#r2 = Some v ->
  e#r2 = Vlong n ->
  let (op, args) := make_modluimm n r1 r2 in
  exists w, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some w /\ Val.lessdef v w.
Proof.
  intros; unfold make_modluimm.
  destruct (Int64.is_power2 n) eqn:?.
  exists v; split; auto. simpl. decEq.
  rewrite H0 in H. destruct (e#r1); inv H. destruct (Int64.eq n Int64.zero); inv H2.
  simpl. erewrite Int64.modu_and by eauto. auto.
  exists v; auto.
Qed.

Lemma make_andlimm_correct:
  forall n r x,
  let (op, args) := make_andlimm n r x in
  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some v /\ Val.lessdef (Val.andl e#r (Vlong n)) v.
Proof.
  intros; unfold make_andlimm.
  predSpec Int64.eq Int64.eq_spec n Int64.zero; intros.
  subst n. exists (Vlong Int64.zero); split; auto. destruct (e#r); simpl; auto. rewrite Int64.and_zero; auto.
  predSpec Int64.eq Int64.eq_spec n Int64.mone; intros.
  subst n. exists (e#r); split; auto. destruct (e#r); simpl; auto. rewrite Int64.and_mone; auto.
  econstructor; split; eauto. auto.
Qed.

Lemma make_orlimm_correct:
  forall n r,
  let (op, args) := make_orlimm n r in
  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some v /\ Val.lessdef (Val.orl e#r (Vlong n)) v.
Proof.
  intros; unfold make_orlimm.
  predSpec Int64.eq Int64.eq_spec n Int64.zero; intros.
  subst n. exists (e#r); split; auto. destruct (e#r); simpl; auto. rewrite Int64.or_zero; auto.
  predSpec Int64.eq Int64.eq_spec n Int64.mone; intros.
  subst n. exists (Vlong Int64.mone); split; auto. destruct (e#r); simpl; auto. rewrite Int64.or_mone; auto.
  econstructor; split; eauto. auto.
Qed.

Lemma make_xorlimm_correct:
  forall n r,
  let (op, args) := make_xorlimm n r in
  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some v /\ Val.lessdef (Val.xorl e#r (Vlong n)) v.
Proof.
  intros; unfold make_xorlimm.
  predSpec Int64.eq Int64.eq_spec n Int64.zero; intros.
  subst n. exists (e#r); split; auto. destruct (e#r); simpl; auto. rewrite Int64.xor_zero; auto.
  predSpec Int64.eq Int64.eq_spec n Int64.mone; intros.
  subst n. exists (Val.notl e#r); split; auto.
  econstructor; split; eauto. auto.
Qed.

Lemma make_mulfimm_correct:
  forall n r1 r2,
  e#r2 = Vfloat n ->
  let (op, args) := make_mulfimm n r1 r1 r2 in
  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some v /\ Val.lessdef (Val.mulf e#r1 e#r2) v.
Proof.
  intros; unfold make_mulfimm.
  destruct (Float.eq_dec n (Float.of_int (Int.repr 2))); intros.
  simpl. econstructor; split. eauto. rewrite H; subst n.
  destruct (e#r1); simpl; auto. rewrite Float.mul2_add; auto.
  simpl. econstructor; split; eauto.
Qed.

Lemma make_mulfimm_correct_2:
  forall n r1 r2,
  e#r1 = Vfloat n ->
  let (op, args) := make_mulfimm n r2 r1 r2 in
  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some v /\ Val.lessdef (Val.mulf e#r1 e#r2) v.
Proof.
  intros; unfold make_mulfimm.
  destruct (Float.eq_dec n (Float.of_int (Int.repr 2))); intros.
  simpl. econstructor; split. eauto. rewrite H; subst n.
  destruct (e#r2); simpl; auto. rewrite Float.mul2_add; auto.
  rewrite Float.mul_commut; auto.
  simpl. econstructor; split; eauto.
Qed.

Lemma make_mulfsimm_correct:
  forall n r1 r2,
  e#r2 = Vsingle n ->
  let (op, args) := make_mulfsimm n r1 r1 r2 in
  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some v /\ Val.lessdef (Val.mulfs e#r1 e#r2) v.
Proof.
  intros; unfold make_mulfsimm.
  destruct (Float32.eq_dec n (Float32.of_int (Int.repr 2))); intros.
  simpl. econstructor; split. eauto. rewrite H; subst n.
  destruct (e#r1); simpl; auto. rewrite Float32.mul2_add; auto.
  simpl. econstructor; split; eauto.
Qed.

Lemma make_mulfsimm_correct_2:
  forall n r1 r2,
  e#r1 = Vsingle n ->
  let (op, args) := make_mulfsimm n r2 r1 r2 in
  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some v /\ Val.lessdef (Val.mulfs e#r1 e#r2) v.
Proof.
  intros; unfold make_mulfsimm.
  destruct (Float32.eq_dec n (Float32.of_int (Int.repr 2))); intros.
  simpl. econstructor; split. eauto. rewrite H; subst n.
  destruct (e#r2); simpl; auto. rewrite Float32.mul2_add; auto.
  rewrite Float32.mul_commut; auto.
  simpl. econstructor; split; eauto.
Qed.

Lemma make_cast8signed_correct:
  forall r x,
  vmatch bc e#r x ->
  let (op, args) := make_cast8signed r x in
  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some v /\ Val.lessdef (Val.sign_ext 8 e#r) v.
Proof.
  intros; unfold make_cast8signed. destruct (vincl x (Sgn Ptop 8)) eqn:INCL.
  exists e#r; split; auto.
  assert (V: vmatch bc e#r (Sgn Ptop 8)).
  { eapply vmatch_ge; eauto. apply vincl_ge; auto. }
  inv V; simpl; auto. rewrite is_sgn_sign_ext in H4 by auto. rewrite H4; auto.
  econstructor; split; simpl; eauto.
Qed.

Lemma make_cast8unsigned_correct:
  forall r x,
  vmatch bc e#r x ->
  let (op, args) := make_cast8unsigned r x in
  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some v /\ Val.lessdef (Val.zero_ext 8 e#r) v.
Proof.
  intros; unfold make_cast8unsigned. destruct (vincl x (Uns Ptop 8)) eqn:INCL.
  exists e#r; split; auto.
  assert (V: vmatch bc e#r (Uns Ptop 8)).
  { eapply vmatch_ge; eauto. apply vincl_ge; auto. }
  inv V; simpl; auto. rewrite is_uns_zero_ext in H4 by auto. rewrite H4; auto.
  econstructor; split; simpl; eauto.
Qed.

Lemma make_cast16signed_correct:
  forall r x,
  vmatch bc e#r x ->
  let (op, args) := make_cast16signed r x in
  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some v /\ Val.lessdef (Val.sign_ext 16 e#r) v.
Proof.
  intros; unfold make_cast16signed. destruct (vincl x (Sgn Ptop 16)) eqn:INCL.
  exists e#r; split; auto.
  assert (V: vmatch bc e#r (Sgn Ptop 16)).
  { eapply vmatch_ge; eauto. apply vincl_ge; auto. }
  inv V; simpl; auto. rewrite is_sgn_sign_ext in H4 by auto. rewrite H4; auto.
  econstructor; split; simpl; eauto.
Qed.

Lemma make_cast16unsigned_correct:
  forall r x,
  vmatch bc e#r x ->
  let (op, args) := make_cast16unsigned r x in
  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some v /\ Val.lessdef (Val.zero_ext 16 e#r) v.
Proof.
  intros; unfold make_cast16unsigned. destruct (vincl x (Uns Ptop 16)) eqn:INCL.
  exists e#r; split; auto.
  assert (V: vmatch bc e#r (Uns Ptop 16)).
  { eapply vmatch_ge; eauto. apply vincl_ge; auto. }
  inv V; simpl; auto. rewrite is_uns_zero_ext in H4 by auto. rewrite H4; auto.
  econstructor; split; simpl; eauto.
Qed.

Lemma op_strength_reduction_correct:
  forall op args vl v,
  vl = map (fun r => AE.get r ae) args ->
  eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some v ->
  let (op', args') := op_strength_reduction op args vl in
  exists w, eval_operation ge (Vptr sp Ptrofs.zero) op' e##args' m = Some w /\ Val.lessdef v w.
Proof.
  intros until v; unfold op_strength_reduction;
  case (op_strength_reduction_match op args vl); simpl; intros.
(* cast8signed *)
  InvApproxRegs; SimplVM; inv H0. apply make_cast8signed_correct; auto.
(* cast8unsigned *)
  InvApproxRegs; SimplVM; inv H0. apply make_cast8unsigned_correct; auto.
(* cast16signed *)
  InvApproxRegs; SimplVM; inv H0. apply make_cast16signed_correct; auto.
(* cast16unsigned *)
  InvApproxRegs; SimplVM; inv H0. apply make_cast16unsigned_correct; auto.
(* sub *)
  InvApproxRegs; SimplVM; inv H0. rewrite Val.sub_add_opp. apply make_addimm_correct; auto.
(* mul *)
  rewrite Val.mul_commut in H0. InvApproxRegs; SimplVM; inv H0. apply make_mulimm_correct; auto.
  InvApproxRegs; SimplVM; inv H0. apply make_mulimm_correct; auto.
(* divs *)
  assert (e#r2 = Vint n2). clear H0. InvApproxRegs; SimplVM; auto.
  apply make_divimm_correct; auto.
(* divu *)
  assert (e#r2 = Vint n2). clear H0. InvApproxRegs; SimplVM; auto.
  apply make_divuimm_correct; auto.
(* modu *)
  assert (e#r2 = Vint n2). clear H0. InvApproxRegs; SimplVM; auto.
  apply make_moduimm_correct; auto.
(* and *)
  rewrite Val.and_commut in H0. InvApproxRegs; SimplVM; inv H0. apply make_andimm_correct; auto.
  InvApproxRegs; SimplVM; inv H0. apply make_andimm_correct; auto.
  inv H; inv H0. apply make_andimm_correct; auto.
(* or *)
  rewrite Val.or_commut in H0. InvApproxRegs; SimplVM; inv H0. apply make_orimm_correct; auto.
  InvApproxRegs; SimplVM; inv H0. apply make_orimm_correct; auto.
(* xor *)
  rewrite Val.xor_commut in H0. InvApproxRegs; SimplVM; inv H0. apply make_xorimm_correct; auto.
  InvApproxRegs; SimplVM; inv H0. apply make_xorimm_correct; auto.
(* shl *)
  InvApproxRegs; SimplVM; inv H0. apply make_shlimm_correct; auto.
(* shr *)
  InvApproxRegs; SimplVM; inv H0. apply make_shrimm_correct; auto.
(* shru *)
  InvApproxRegs; SimplVM; inv H0. apply make_shruimm_correct; auto.
(* lea *)
  exploit addr_strength_reduction_32_correct; eauto.
  destruct (addr_strength_reduction_32 addr args0 vl0) as [addr' args'].
  auto.
(* subl *)
  InvApproxRegs; SimplVM; inv H0.
  replace (Val.subl e#r1 (Vlong n2)) with (Val.addl e#r1 (Vlong (Int64.neg n2))).
  apply make_addlimm_correct; auto.
  unfold Val.addl, Val.subl. destruct Archi.ptr64 eqn:SF, e#r1; auto.
  rewrite Int64.sub_add_opp; auto.
  rewrite Ptrofs.sub_add_opp. do 2 f_equal. auto with ptrofs.
  rewrite Int64.sub_add_opp; auto.
(* mull *)
  rewrite Val.mull_commut in H0. InvApproxRegs; SimplVM; inv H0. apply make_mullimm_correct; auto.
  InvApproxRegs; SimplVM; inv H0. apply make_mullimm_correct; auto.
(* divl *)
  assert (e#r2 = Vlong n2). clear H0. InvApproxRegs; SimplVM; auto.
  apply make_divlimm_correct; auto.
(* divlu *)
  assert (e#r2 = Vlong n2). clear H0. InvApproxRegs; SimplVM; auto.
  apply make_divluimm_correct; auto.
(* modlu *)
  assert (e#r2 = Vlong n2). clear H0. InvApproxRegs; SimplVM; auto.
  apply make_modluimm_correct; auto.
(* andl *)
  rewrite Val.andl_commut in H0. InvApproxRegs; SimplVM; inv H0. apply make_andlimm_correct; auto.
  InvApproxRegs; SimplVM; inv H0. apply make_andlimm_correct; auto.
  inv H; inv H0. apply make_andlimm_correct; auto.
(* orl *)
  rewrite Val.orl_commut in H0. InvApproxRegs; SimplVM; inv H0. apply make_orlimm_correct; auto.
  InvApproxRegs; SimplVM; inv H0. apply make_orlimm_correct; auto.
(* xorl *)
  rewrite Val.xorl_commut in H0. InvApproxRegs; SimplVM; inv H0. apply make_xorlimm_correct; auto.
  InvApproxRegs; SimplVM; inv H0. apply make_xorlimm_correct; auto.
(* shll *)
  InvApproxRegs; SimplVM; inv H0. apply make_shllimm_correct; auto.
(* shrl *)
  InvApproxRegs; SimplVM; inv H0. apply make_shrlimm_correct; auto.
(* shrlu *)
  InvApproxRegs; SimplVM; inv H0. apply make_shrluimm_correct; auto.
(* leal *)
  exploit addr_strength_reduction_64_correct; eauto.
  destruct (addr_strength_reduction_64 addr args0 vl0) as [addr' args'].
  auto.
(* cond *)
  inv H0. apply make_cmp_correct; auto.
(* mulf *)
  InvApproxRegs; SimplVM; inv H0. rewrite <- H2. apply make_mulfimm_correct; auto.
  InvApproxRegs; SimplVM; inv H0. fold (Val.mulf (Vfloat n1) e#r2).
  rewrite <- H2. apply make_mulfimm_correct_2; auto.
(* mulfs *)
  InvApproxRegs; SimplVM; inv H0. rewrite <- H2. apply make_mulfsimm_correct; auto.
  InvApproxRegs; SimplVM; inv H0. fold (Val.mulfs (Vsingle n1) e#r2).
  rewrite <- H2. apply make_mulfsimm_correct_2; auto.
(* default *)
  exists v; auto.
Qed.

End STRENGTH_REDUCTION.

author: CertiKOS


text:
Require Import Coq.Program.Equality.
Require Import Coq.Program.Tactics.
Require Export DeclarationEvaluation.
Require Export DeclarationTyping.

(******************************************************************************)
(* Weakening lemmas                                                           *)
(******************************************************************************)

Lemma PTyping_bindPat_domainEnv {Γ p T Δ} (wp: PTyping Γ p T Δ) :
  bindPat p = domainEnv Δ.
Proof.
  induction wp; isimpl; congruence.
Qed.

Lemma shift_evar_ptyping {Γ1 p T Δ} (wt: PTyping Γ1 p T Δ) :
  ∀ {c Γ2}, shift_evar c Γ1 Γ2 → PTyping Γ2 p T Δ.
Proof.
  induction wt; econstructor; eauto with infra.
Qed.

Lemma shift_evar_typing {Γ1 t T} (wt: Typing Γ1 t T) :
  ∀ {c Γ2}, shift_evar c Γ1 Γ2 → Typing Γ2 (shiftTm c t) T.
Proof.
  induction wt; simpl; intros; try (econstructor; eauto with infra; fail).
  - rewrite (PTyping_bindPat_domainEnv H).
    econstructor; eauto using shift_evar_ptyping with infra.
Qed.

Lemma weaken_typing {Γ} Δ :
  ∀ {t T}, Typing Γ t T → Typing (appendEnv Γ Δ) (weakenTm t (domainEnv Δ)) T.
Proof.
  induction Δ; simpl; eauto using shift_evar_typing with infra.
Qed.

Lemma shift_value {t} :
  ∀ {c}, Value t → Value (shiftTm c t).
Proof.
  induction t; simpl; intros; try contradiction; destruct_conjs; auto.
Qed.

Lemma weaken_value u :
  ∀ {t}, Value t → Value (weakenTm t u).
Proof.
  induction u as [|[]]; simpl; auto using shift_value.
Qed.

(******************************************************************************)
(* Substitution lemmas                                                        *)
(******************************************************************************)

Lemma subst_evar_ptyping {Γ s S} (wts: Typing Γ s S)
  {Γ1 p T Δ} (wp: PTyping Γ1 p T Δ) :
  ∀ {x Γ2}, subst_evar Γ S s x Γ1 Γ2 → PTyping Γ2 p T Δ.
Proof.
  induction wp; simpl; econstructor; eauto with infra.
Qed.

Lemma subst_evar_lookup_evar {Γ s S} (wt: Typing Γ s S)
  {x Γ1 Γ2} (esub: subst_evar Γ S s x Γ1 Γ2) :
  ∀ {y T}, lookup_evar Γ1 y T → Typing Γ2 (substIndex x s y) T.
Proof.
  induction esub; inversion 1; subst; simpl;
    eauto using T_Var, shift_evar_typing with infra.
Qed.

Lemma subst_evar_typing {Γ s S Γ1 t T} (wts: Typing Γ s S) (wt: Typing Γ1 t T) :
  ∀ {x Γ2}, subst_evar Γ S s x Γ1 Γ2 → Typing Γ2 (substTm x s t) T.
Proof.
  induction wt; simpl; intros; eauto using subst_evar_lookup_evar;
    try (econstructor; eauto with infra; fail).
  - rewrite (PTyping_bindPat_domainEnv H).
    eapply T_Let; eauto using subst_evar_ptyping with infra.
Qed.

(******************************************************************************)
(* Progress                                                                   *)
(******************************************************************************)

Lemma can_form_tarr {Γ t T1 T2} (v: Value t) (wt: Typing Γ t (tarr T1 T2)) :
  ∃ t2, t = abs T1 t2.
Proof.
  depind wt; try contradiction; exists t; reflexivity.
Qed.

Lemma can_form_tprod {Γ t T1 T2} (v: Value t) (wt: Typing Γ t (tprod T1 T2)) :
  ∃ t1 t2, t = prod t1 t2 ∧ Typing Γ t1 T1 ∧ Typing Γ t2 T2.
Proof.
  depind wt; try contradiction; exists t1, t2; split; auto.
Qed.

Lemma matching_defined {Γ p T1 Δ} (wp: PTyping Γ p T1 Δ) :
  ∀ {t1}, Value t1 → Typing Γ t1 T1 → ∀ t2, ∃ t2', Match p t1 t2 t2'.
Proof.
  induction wp; intros t1 v1 wt1 t2.
  - exists (substTm X0 t1 t2).
    refine M_Var.
  - destruct (can_form_tprod v1 wt1) as (t11 & t12 & eq & wt11 & wt12); subst.
    destruct v1 as [v11 v12].
    apply (weaken_typing Δ1) in wt12.
    assert (val12' : Value (weakenTm t12 (domainEnv Δ1)))
       by (apply weaken_value; auto).
    destruct (IHwp2 (weakenTm t12 (domainEnv Δ1)) val12' wt12 t2) as [t2' m2].
    destruct (IHwp1 _ v11 wt11 t2') as [t2'' m1].
    rewrite <- (PTyping_bindPat_domainEnv wp1) in m2.
    exists t2''.
    exact (M_Prod m2 m1).
Qed.

Lemma progress {t U} (wt: Typing empty t U) :
  Value t ∨ ∃ t', red t t'.
Proof with try (subst; eauto using red).
  depind wt; simpl; auto.
  - inversion H.
  - destruct IHwt1 as [v1|[t1' r1]]...
    destruct IHwt2 as [v2|[t2' r2]]...
    destruct (can_form_tarr v1 wt1)...
  - destruct IHwt1 as [v1|[t1' r1]]...
    destruct IHwt2 as [v2|[t2' r2]]...
  - destruct IHwt1 as [v1|[t1' r1]]...
    destruct (matching_defined H v1 wt1 t2)...
Qed.

(******************************************************************************)
(* Preservation                                                               *)
(******************************************************************************)

Lemma local_preservation_lett {p t1 t2 t2'} (m: Match p t1 t2 t2') :
  ∀ {Γ T1 T2 Δ}, PTyping Γ p T1 Δ → Typing Γ t1 T1 →
    Typing (appendEnv Γ Δ) t2 T2 → Typing Γ t2' T2.
Proof.
  induction m; intros Γ T1 T2 Δ wtp wt1 wt2.
  - dependent destruction wtp.
    eauto using subst_evar_typing with infra.
  - dependent destruction wtp.
    dependent destruction wt1.
    rewrite (PTyping_bindPat_domainEnv wtp1) in *.
    rewrite appendEnv_assoc in wt2.
    eauto using weaken_typing.
Qed.

Lemma preservation {Γ t U} (wt: Typing Γ t U) :
  ∀ {t'}, red t t' → Typing Γ t' U.
Proof.
  induction wt; intros t' r; inversion r; subst;
    eauto using Typing, local_preservation_lett.
  - inversion wt1; eauto using subst_evar_typing with infra.
Qed.

author: skeuchel

repo: metatheory

save_path: github-repos/coq/skeuchel-metatheory


text:
From Test Require Import tactic.

Section FOFProblem.

Variable Universe : Set.
Variable UniverseElement : Universe.

Variable p_ : Universe -> Universe -> Universe -> Universe -> Universe -> Universe -> Universe -> Universe -> Universe -> Universe -> Universe -> Universe -> Universe -> Universe -> Universe -> Universe -> Universe -> Universe -> Universe -> Universe -> Universe -> Universe -> Universe -> Universe -> Universe -> Universe -> Universe -> Universe -> Universe -> Universe -> Universe -> Universe -> Universe -> Universe -> Universe -> Universe -> Universe -> Universe -> Universe -> Universe -> Universe -> Universe -> Universe -> Prop.
Variable goal_ : Prop.
Variable dom_ : Universe -> Prop.

Variable a9_ : Universe.
Variable a8_ : Universe.
Variable a7_ : Universe.
Variable a6_ : Universe.
Variable a5_ : Universe.
Variable a43_ : Universe.
Variable a42_ : Universe.
Variable a41_ : Universe.
Variable a40_ : Universe.
Variable a4_ : Universe.
Variable a39_ : Universe.
Variable a38_ : Universe.
Variable a37_ : Universe.
Variable a36_ : Universe.
Variable a35_ : Universe.
Variable a34_ : Universe.
Variable a33_ : Universe.
Variable a32_ : Universe.
Variable a31_ : Universe.
Variable a30_ : Universe.
Variable a3_ : Universe.
Variable a29_ : Universe.
Variable a28_ : Universe.
Variable a27_ : Universe.
Variable a26_ : Universe.
Variable a25_ : Universe.
Variable a24_ : Universe.
Variable a23_ : Universe.
Variable a22_ : Universe.
Variable a21_ : Universe.
Variable a20_ : Universe.
Variable a2_ : Universe.
Variable a19_ : Universe.
Variable a18_ : Universe.
Variable a17_ : Universe.
Variable a16_ : Universe.
Variable a15_ : Universe.
Variable a14_ : Universe.
Variable a13_ : Universe.
Variable a12_ : Universe.
Variable a11_ : Universe.
Variable a10_ : Universe.
Variable a1_ : Universe.

Variable ax1_1 : (dom_ a1_ /\ (dom_ a2_ /\ (dom_ a3_ /\ (dom_ a4_ /\ (dom_ a5_ /\ (dom_ a6_ /\ (dom_ a7_ /\ (dom_ a8_ /\ (dom_ a9_ /\ (dom_ a10_ /\ (dom_ a11_ /\ (dom_ a12_ /\ (dom_ a13_ /\ (dom_ a14_ /\ (dom_ a15_ /\ (dom_ a16_ /\ (dom_ a17_ /\ (dom_ a18_ /\ (dom_ a19_ /\ (dom_ a20_ /\ (dom_ a21_ /\ (dom_ a22_ /\ (dom_ a23_ /\ (dom_ a24_ /\ (dom_ a25_ /\ (dom_ a26_ /\ (dom_ a27_ /\ (dom_ a28_ /\ (dom_ a29_ /\ (dom_ a30_ /\ (dom_ a31_ /\ (dom_ a32_ /\ (dom_ a33_ /\ (dom_ a34_ /\ (dom_ a35_ /\ (dom_ a36_ /\ (dom_ a37_ /\ (dom_ a38_ /\ (dom_ a39_ /\ (dom_ a40_ /\ (dom_ a41_ /\ (dom_ a42_ /\ dom_ a43_)))))))))))))))))))))))))))))))))))))))))).
Variable ax2_2 : (forall A1 A2 A3 A4 A5 A6 A7 A8 A9 A10 A11 A12 A13 A14 A15 A16 A17 A18 A19 A20 A21 A22 A23 A24 A25 A26 A27 A28 A29 A30 A31 A32 A33 A34 A35 A36 A37 A38 A39 A40 A41 A42 A43 : Universe, ((dom_ A1 /\ (dom_ A2 /\ (dom_ A3 /\ (dom_ A4 /\ (dom_ A5 /\ (dom_ A6 /\ (dom_ A7 /\ (dom_ A8 /\ (dom_ A9 /\ (dom_ A10 /\ (dom_ A11 /\ (dom_ A12 /\ (dom_ A13 /\ (dom_ A14 /\ (dom_ A15 /\ (dom_ A16 /\ (dom_ A17 /\ (dom_ A18 /\ (dom_ A19 /\ (dom_ A20 /\ (dom_ A21 /\ (dom_ A22 /\ (dom_ A23 /\ (dom_ A24 /\ (dom_ A25 /\ (dom_ A26 /\ (dom_ A27 /\ (dom_ A28 /\ (dom_ A29 /\ (dom_ A30 /\ (dom_ A31 /\ (dom_ A32 /\ (dom_ A33 /\ (dom_ A34 /\ (dom_ A35 /\ (dom_ A36 /\ (dom_ A37 /\ (dom_ A38 /\ (dom_ A39 /\ (dom_ A40 /\ (dom_ A41 /\ (dom_ A42 /\ dom_ A43)))))))))))))))))))))))))))))))))))))))))) -> p_ A1 A2 A3 A4 A5 A6 A7 A8 A9 A10 A11 A12 A13 A14 A15 A16 A17 A18 A19 A20 A21 A22 A23 A24 A25 A26 A27 A28 A29 A30 A31 A32 A33 A34 A35 A36 A37 A38 A39 A40 A41 A42 A43)).
Variable ax3_3 : (p_ a43_ a42_ a41_ a40_ a39_ a38_ a37_ a36_ a35_ a34_ a33_ a32_ a31_ a30_ a29_ a28_ a27_ a26_ a25_ a24_ a23_ a22_ a21_ a20_ a19_ a18_ a17_ a16_ a15_ a14_ a13_ a12_ a11_ a10_ a9_ a8_ a7_ a6_ a5_ a4_ a3_ a2_ a1_ -> goal_).

Theorem lemma43_4 : goal_.
Proof.
  time tac.
Qed.

End FOFProblem.

author: janicicpredrag

repo: Larus

save_path: github-repos/coq/janicicpredrag-Larus


text:
(*
 * 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 String.
Require Import EJsonRuntime.
Require Import Imp.
Require Import ImpEJson.
Require Import ImpEJsonEval.
Require Import ImpEJsonRewrite.
Require Import ImpEJsonBlockRewrite.

(* XXX This is a temporary place-holder, includes only for loop rewrites *)
Section ImpEJsonOptimizer.
  Context {foreign_ejson_model:Set}.
  Context {fejson:foreign_ejson foreign_ejson_model}.
  Context {foreign_ejson_runtime_op : Set}.
  Context {fejruntime:foreign_ejson_runtime foreign_ejson_runtime_op}.

  Definition imp_ejson_optim_top (q:@imp_ejson foreign_ejson_model foreign_ejson_runtime_op) : imp_ejson :=
    imp_ejson_block_rewrite
      (imp_ejson_rewrite q).

  Section Correctness.
    Lemma imp_ejson_optim_top_correct h (σ : list (string * ejson)) (q:imp_ejson) :
        imp_ejson_eval_top_on_ejson h σ q =
        imp_ejson_eval_top_on_ejson h σ (imp_ejson_optim_top q).
    Proof.
      unfold imp_ejson_eval_top_on_ejson.
      unfold imp_ejson_optim_top.
      rewrite imp_ejson_rewrite_correct.
      rewrite imp_ejson_block_rewrite_correct.
      reflexivity.
    Qed.

  End Correctness.
End ImpEJsonOptimizer.

author: querycert

repo: qcert

save_path: github-repos/coq/querycert-qcert