text:
From Equations Require Import Equations.
From Coq Require Import ssreflect.
From MetaCoq.Template Require Import config utils.
From MetaCoq.Template Require Ast TypingWf WfAst TermEquality EtaExpand TemplateProgram.
From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils PCUICCumulativity
     PCUICLiftSubst PCUICEquality PCUICReduction
     PCUICUnivSubst PCUICTyping PCUICGlobalEnv TemplateToPCUIC
     PCUICWeakeningConv PCUICWeakeningTyp PCUICSubstitution PCUICGeneration
     PCUICCasesContexts TemplateToPCUICCorrectness PCUICEtaExpand
     PCUICProgram.

Tactic Notation "wf_inv" ident(H) simple_intropattern(p) :=
(eapply WfAst.wf_inv in H; progress cbn in H; try destruct H as p) ||
(apply WfAst.wf_mkApps_napp in H; [|easy]; try destruct H as p).

Local Hint Constructors expanded : expanded.

Lemma expanded_context_map2_bias_left Σ n bctx ctx :
  #|ctx| = #|bctx| ->
  expanded_context Σ n ctx ->
  expanded_context Σ n
     (map2_bias_left set_binder_name dummy_decl bctx ctx).
Proof.
  unfold expanded_context.
  intros hl.
  rewrite map2_map2_bias_left //.
  intros [a]. sq.
  induction a in bctx, hl |- *; try econstructor; auto.
  - cbn. destruct bctx; constructor.
  - destruct bctx => //.
    cbn. constructor; auto. cbn.
    destruct (decl_body d); constructor => //. depelim p.
    cbn in hl. assert (#|Γ| = #|bctx|) by lia.
    rewrite map2_length //. now rewrite -H0.
Qed.

Import PCUICWeakeningEnv.
(* TODO move *)
Lemma extends_decls_trans Σ Σ' Σ'' : extends_decls Σ Σ' -> extends_decls Σ' Σ'' -> extends_decls Σ Σ''.
Proof.
  intros [e [ext e'] er] [e0 [ext' e0'] er']. subst. split. now transitivity Σ'.
  exists (ext' ++ ext). now rewrite -app_assoc.
  congruence.
Qed.

Lemma declared_minductive_expanded Σ c mdecl :
  expanded_global_env Σ ->
  declared_minductive Σ c mdecl ->
  exists Σ', ∥ extends_decls Σ' Σ ∥ /\ expanded_minductive_decl Σ' mdecl.
Proof.
  unfold expanded_global_env, declared_minductive, lookup_env.
  destruct Σ as [univs Σ]; cbn. unfold declared_minductive_gen.
  intros exp; induction exp; cbn => //.
  destruct decl as [kn d]; cbn.
  destruct (eqb_spec c kn). intros [= ->].
  subst c. eexists. split ; [|exact H]. sq. red. split => //. cbn.
  eexists. cbn. instantiate (1:= [_]); reflexivity.
  intros hl; destruct (IHexp hl). exists x. intuition auto.
  sq. eapply extends_decls_trans; tea.
  split => //. now exists [(kn, d)].
Qed.

Lemma declared_constructor_expanded {Σ c mdecl idecl cdecl} :
  expanded_global_env Σ ->
  declared_constructor Σ c mdecl idecl cdecl ->
  exists Σ', ∥ extends_decls Σ' Σ ∥ /\ expanded_minductive_decl Σ' mdecl /\ expanded_constructor_decl Σ' mdecl cdecl.
Proof.
  intros exp [[decli hnth] hnth'].
  eapply declared_minductive_expanded in decli.
  destruct decli as [Σ' [ext exp']]. exists Σ'; split => //. split => //.
  destruct exp' as [hp hb]. solve_all.
  eapply nth_error_all in hb; tea.
  destruct hb as [hb]. solve_all.
  eapply nth_error_all in hb; tea.
  auto.
Qed.

Lemma expanded_extended_subst {Σ Γ Δ} :
  expanded_context Σ Γ Δ ->
  forall n,
  Forall (expanded Σ (repeat 0 (n + context_assumptions Δ) ++ Γ)) (extended_subst Δ n).
Proof.
  intros [a]; induction a. cbn. constructor.
  cbn. destruct d as [na [b|] ty]; cbn in *. constructor; auto.
  { cbn. eapply (expanded_subst _ _ 0 _ []) => //. cbn. rewrite -/(repeat _ _).
    specialize (IHa n). solve_all.
    len. rewrite repeat_app Nat.add_comm.
    eapply expanded_lift. 1-2:now len; rewrite !repeat_length.
    now depelim p. }
  constructor; auto.
  eapply (expanded_tRel _ _ _ _ []) => //. cbn.
  rewrite nth_error_app_lt. rewrite repeat_length. lia.
  rewrite nth_error_repeat //. lia.
  specialize (IHa (S n)).
  now rewrite Nat.add_succ_r.
Qed.

Lemma expanded_let_expansion {Σ} {Δ : context} {Γ t} :
  expanded_context Σ Γ Δ ->
  expanded_context Σ (repeat 0 #|Δ| ++ Γ) t ->
  expanded_context Σ (repeat 0 (context_assumptions Δ) ++ Γ) (expand_lets_ctx Δ t).
Proof.
  rewrite /expanded_context.
  intros [aΔ] [a]; sq.
  unfold expand_lets_ctx, expand_lets_k_ctx.
  do 2 eapply PCUICParallelReduction.All_fold_fold_context_k.
  eapply All_fold_impl; tea. cbn.
  intros Γ' x f. destruct (decl_body x) => //; constructor.
  len. depelim f.
  eapply expanded_subst. now rewrite repeat_length.
  clear -aΔ. eapply (expanded_extended_subst (sq aΔ) 0).
  len. rewrite app_assoc -repeat_app. eapply expanded_lift. len. now rewrite !repeat_length.
  now rewrite repeat_length. rewrite repeat_app -app_assoc //.
Qed.

Lemma expanded_context_subst {Σ} {Δ Δ' : list nat} {Γ s k t} :
  #|s| = #|Δ'| ->
  #|Δ| = k ->
  Forall (expanded Σ Γ) s ->
  expanded_context Σ (Δ ++ repeat 0 #|Δ'| ++ Γ) t ->
  expanded_context Σ (Δ ++ Γ) (subst_context s k t).
Proof.
  intros hs hs' has.
  rewrite /expanded_context.
  intros [aΔ]; sq.
  eapply PCUICParallelReduction.All_fold_fold_context_k.
  eapply All_fold_impl; tea. cbn.
  intros Γ' x f. destruct (decl_body x) => //; constructor.
  len. depelim f. rewrite app_assoc.
  eapply expanded_subst. len. rewrite repeat_length. lia. solve_all. auto.
  now rewrite -app_assoc hs.
Qed.

Lemma expanded_inds {Σ Γ ind u bodies} : Forall (expanded Σ Γ) (inds ind u bodies).
Proof.
  unfold inds. induction #|bodies|; cbn; auto. constructor => //. constructor.
Qed.

Implicit Types (cf : checker_flags).

Lemma expanded_weakening {cf} {Σ Σ' Γ t} :
  wf Σ' -> extends_decls Σ Σ' -> expanded Σ Γ t -> expanded Σ' Γ t.
Proof.
  intros wfΣ ext.
  eapply expanded_ind; intros.
  all:try solve [econstructor; eauto].
  - econstructor; eauto. solve_all. sq. eapply All_fold_impl; tea; cbn.
    intros ? ? []; constructor; auto. now rewrite <- repeat_app.
  - eapply expanded_tFix; tea; eauto. solve_all.
  - eapply expanded_tConstruct_app; tea.
    eapply weakening_env_declared_constructor; tea. now eapply extends_decls_extends.
Qed.

Lemma expanded_context_weakening {cf} {Σ Σ' Γ t} :
  wf Σ' -> extends_decls Σ Σ' -> expanded_context Σ Γ t -> expanded_context Σ' Γ t.
Proof.
  intros wfΣ ext.
  intros [a]; sq.
  eapply All_fold_impl; tea; cbn; eauto.
  intros ?? []; constructor.
  eapply expanded_weakening; eauto.
Qed.

Lemma expanded_bcontext {cf} Σ ind k mdecl idecl cdecl bctx bbody :
  wf Σ ->
  PCUICEtaExpand.expanded_global_env Σ ->
  #|cstr_branch_context ind mdecl cdecl| = #|bctx| ->
  declared_constructor Σ (ind, k) mdecl idecl cdecl ->
  expanded_context Σ (repeat 0 (context_assumptions mdecl.(ind_params))) (bcontext (trans_branch ind mdecl cdecl bctx bbody)).
Proof.
  intros wfΣ expΣ hl declc.
  eapply expanded_context_map2_bias_left => //.
  destruct (declared_constructor_expanded expΣ declc) as [Σ' [ext [expm expc]]].
  destruct expm as [hp hb]. destruct expc as [hargs].
  unfold cstr_branch_context.
  epose proof (expanded_let_expansion hp (t:=(subst_context
  (inds (inductive_mind ind) (abstract_instance (ind_universes mdecl))
     (ind_bodies mdecl)) #|ind_params mdecl|
  (cstr_args cdecl)))).
  rewrite !app_nil_r in H. forward H.
  epose proof (expanded_context_subst (Γ := []) (Δ' := repeat 0 #|ind_bodies mdecl|)).
  rewrite !app_nil_r in H0. eapply H0; rewrite ?repeat_length //. len. apply expanded_inds.
  rewrite -repeat_app. exact hargs.
  destruct ext. eapply expanded_context_weakening; tea.
Qed.

Lemma trans_expanded {cf : checker_flags} {Σ} {wfΣ : Template.Typing.wf Σ} Γ T  :
  let Σ' := trans_global_env Σ in
  WfAst.wf Σ T ->
  PCUICEtaExpand.expanded_global_env Σ' ->
  EtaExpand.expanded Σ Γ T ->
  expanded Σ' Γ (trans Σ' T).
Proof with eauto using expanded.
  intros Σ' wf expΣ' exp. revert wf.
  induction exp; intros wf; cbn -[Σ']...
  all: try now (wf_inv wf []; eauto using expanded).
  - wf_inv wf ?. eapply expanded_tRel with (args := []). eauto. lia. econstructor.
  - wf_inv wf [[[]]]. eapply expanded_tRel. eauto. len. solve_all.
  - wf_inv wf [[[]]]. econstructor. solve_all.
  - wf_inv wf []. cbn. eapply expanded_mkApps with (args := [_]); cbn... econstructor.
    eapply expanded_tRel with (args := []). reflexivity. lia. econstructor.
  - try now (wf_inv wf [[]]; eauto using expanded).
  - wf_inv wf [[[]]].
    forward IHexp; eauto.
    eapply expanded_mkApps; eauto. 2:solve_all.
    destruct f7; cbn in *; eauto.
    destruct TransLookup.lookup_inductive as [[] | ]; cbn; eauto.
  - wf_inv wf []. eapply forall_decls_declared_constructor in H; eauto. 2: now eapply template_to_pcuic_env.
    eapply expanded_tConstruct_app with (args := []).
    eauto. cbn. unfold trans_local. now rewrite context_assumptions_map. econstructor.
  - wf_inv wf (mdecl' & idecl' & []). eapply forall_decls_declared_inductive in d; eauto. 2: now eapply template_to_pcuic_env.
    unfold Σ'.
    erewrite trans_lookup_inductive, declared_inductive_lookup; eauto.
    econstructor; eauto. cbn.
    + solve_all.
    + cbn. eapply All2_nth_hyp in a1.
      eapply All_Forall, All2_All_map2, All2_map.
      eapply Forall_All in H2. eapply All2_All_mix_right in a1; tea.
      eapply All2_impl; tea. intros x y. cbv beta. intros [[i [Hi []]] ?].
      split.
      { rewrite map_length. relativize #|Ast.pparams type_info|.
        eapply expanded_bcontext => //.
        - now eapply template_to_pcuic_env.
        - len. eapply All2_length in a2. len in a2.
        - split; tea. cbn; rewrite nth_error_map. erewrite Hi => //.
        - cbn. tea. rewrite context_assumptions_map. now rewrite e0. }
      * cbn. rewrite map2_bias_left_length. now eapply e1.
    + eapply template_to_pcuic_env; eauto.
  - now (wf_inv wf [[]]; eauto using expanded).
  - wf_inv wf [[]]. wf_inv w ?. eapply expanded_tFix.
    + solve_all.
      * rewrite trans_isLambda //.
      * revert H2. cbn. now rewrite mapi_cst_map rev_map_spec map_map.
    + solve_all.
    + destruct args; cbn; congruence.
    + now rewrite nth_error_map H5.
    + now simpl_list.
  - wf_inv wf ?. econstructor. solve_all.
  - wf_inv wf [[[]]]. eapply forall_decls_declared_constructor in H; eauto. 2: now eapply template_to_pcuic_env.
    eapply expanded_tConstruct_app. eauto. cbn. unfold trans_local. now rewrite map_length context_assumptions_map. solve_all.
Qed.

Lemma wf_cons_inv {cf} Σ' (Σ : global_declarations) d :
  wf (set_declarations Σ' (d :: Σ)) -> wf (set_declarations Σ' Σ).
Proof.
  intros []. split => //. now depelim o0.
Qed.

Lemma template_wf_cons_inv {cf} univs retro (Σ : Ast.Env.global_declarations) d :
  Typing.wf {| Ast.Env.universes := univs; Ast.Env.declarations := d :: Σ;
    Ast.Env.retroknowledge := retro |} ->
  let Σ' := {| Ast.Env.universes := univs; Ast.Env.declarations := Σ;
    Ast.Env.retroknowledge := retro |} in
  Typing.wf Σ' × Typing.on_global_decl Typing.cumul_gen (WfAst.wf_decl_pred) (Σ', Ast.universes_decl_of_decl d.2) d.1 d.2
  × ST.on_udecl univs (Ast.universes_decl_of_decl d.2).
Proof.
  intros wf; split.
  destruct wf. split => //. now depelim o0.
  eapply typing_wf_wf in wf. depelim wf.
  cbn in o0. depelim o0. cbn. destruct o1. split => //.
  eapply TypingWf.on_global_decl_impl; tea. cbn.
  intros. destruct T => //. red. red in X0. destruct X0. intuition auto.
  cbn. split => //.
Qed.

Lemma trans_global_env_cons univs retro (Σ : Ast.Env.global_declarations) decl :
  trans_global_env {| S.Env.universes := univs; S.Env.declarations := decl :: Σ; S.Env.retroknowledge := retro |} =
  let Σ' := trans_global_env {| S.Env.universes := univs; S.Env.declarations := Σ; S.Env.retroknowledge := retro |} in
  add_global_decl Σ' (decl.1, trans_global_decl Σ' decl.2).
Proof. reflexivity. Qed.

Arguments trans_global_env : simpl never.

Lemma All_fold_map (P : context -> context_decl -> Type) (f : Ast.Env.context_decl -> context_decl) ctx :
  All_fold P (map f ctx) <~> All_fold (fun Γ d => P (map f Γ) (f d)) ctx.
Proof.
  induction ctx.
  - split; constructor.
  - cbn. split; intros H; depelim H; constructor; auto; now apply IHctx.
Qed.

Lemma All_fold_All_mix_left (P : S.Env.context -> S.Env.context_decl -> Type) (Q : S.Env.context_decl -> Type) ctx :
  All_fold P ctx ->
  All Q ctx ->
  All_fold (fun Γ d => Q d × P Γ d) ctx.
Proof.
  induction 1; cbn; intros. constructor.
  depelim X0. constructor; auto.
Qed.

Lemma expanded_trans_local {cf} {Σ} {wfΣ : Typing.wf Σ} Γ ctx :
  expanded_global_env (trans_global_env Σ) ->
  All (WfAst.wf_decl Σ) ctx ->
  EtaExpand.expanded_context Σ Γ ctx ->
  expanded_context (trans_global_env Σ) Γ (trans_local (trans_global_env Σ) ctx).
Proof.
  rewrite /expanded_context.
  intros etaΣ wfctx [a]; split.
  unfold trans_local.
  eapply All_fold_map.
  eapply All_fold_All_mix_left in a; tea.
  eapply All_fold_impl; tea; cbv beta; intros ??; cbn; unfold WfAst.wf_decl;
    intros [wf Hd]; revert Hd wf; intros []; intros [];  constructor; len.
  eapply trans_expanded in H; auto.
Qed.

Lemma wf_context_sorts {cf} {Σ ctx ctx' cunivs} {wfΣ : Typing.wf_ext Σ} :
  Typing.sorts_local_ctx WfAst.wf_decl_pred Σ ctx ctx' cunivs ->
  All (WfAst.wf_decl Σ) ctx'.
Proof.
  induction ctx' in cunivs |- *; cbn; auto.
  destruct a as [na [b|] ty].
  intros [? []]. constructor; auto. eauto.
  destruct cunivs => //.
  intros [? []]. constructor; eauto. constructor; cbn; eauto.
Qed.

Lemma expanded_trans_global_env {cf} Σ {wfΣ : Typing.wf_ext Σ} :
  EtaExpand.expanded_global_env Σ ->
  expanded_global_env (trans_global_env Σ).
Proof.
  destruct Σ as [[univs Σ] udecl].
  cbn -[trans_global_env]. unfold EtaExpand.expanded_global_env; cbn -[trans_global_env].
  intros etaenv; induction etaenv.
  - constructor; auto.
  - destruct wfΣ as [wfΣ onudecl].
    eapply template_wf_cons_inv in wfΣ as [].
    forward IHetaenv by tea. split => //.
    rewrite trans_global_env_cons. set (Σ' := trans_global_env _ ).
    cbv zeta. constructor. apply IHetaenv.
    cbn -[add_global_decl trans_global_env].
    destruct decl as [kn []]; cbn in *; depelim H => //.
    * unfold trans_constant_body; cbn.
      constructor. cbn. destruct p.
      red in o.
      destruct (Ast.Env.cst_body c); cbn => //. cbn in expanded_body.
      eapply trans_expanded in expanded_body; eauto.
      rewrite -/Σ' in expanded_body. now rewrite -eta_global_env.
      red in o. now destruct o.
    * rewrite -eta_global_env.
      constructor.
      + cbn. eapply expanded_trans_local in expanded_params => //.
        destruct p; destruct o. now eapply TypingWf.All_local_env_wf_decls.
      + cbn. destruct p.
        move: o.(Typing.onInductives). destruct o. intros oni.
        eapply All_Forall. eapply Forall_All in expanded_ind_bodies.
        eapply Alli_All_mix in oni; tea. clear expanded_ind_bodies.
        eapply All_map, Alli_All; tea; cbv beta.
        intros n oib []. move: (Typing.onConstructors o).
        intros onc. red in onc.
        destruct e as [expc]. constructor. eapply Forall_All in expc.
        eapply All2_All_mix_left in onc; tea. clear expc. solve_all.
        cbn. solve_all.
        destruct a as [expargs expty]. constructor.
        { cbn. eapply expanded_trans_local in expargs; eauto.
          move: expargs. len.
          move: b.(Typing.on_cargs) => onargs.
          eapply @wf_context_sorts in onargs; tea.
          cbn. split => /= //. exact w. }
Qed.

Import TemplateProgram.

Lemma expanded_trans_program {cf : checker_flags} p (t : wt_template_program p) :
  EtaExpand.expanded_program p ->
  expanded_pcuic_program (trans_template_program p).
Proof.
  intros [etaenv etat].
  destruct t as [? [T HT]]. split.
  unshelve eapply expanded_trans_global_env => //; tc.
  unshelve eapply trans_expanded => //; tc. eapply w.
  now unshelve eapply TypingWf.typing_wf in HT.
  eapply expanded_trans_global_env => //.
Qed.

author: SwampertX

repo: undergraduate-thesis


text:
Require Export XR_Rmult_plus_distr_r.
Require Export XR_Ropp_mult_distr_l.
Require Export XR_Rminus.
Require Export XR_Rdiv.

Local Open Scope R_scope.

Lemma Rdiv_minus_distr : forall a b c, (a - b)/c = a/c - b/c.
Proof.
  intros x y z.
  unfold Rminus, Rdiv.
  rewrite Rmult_plus_distr_r.
  rewrite <- Ropp_mult_distr_l.
  reflexivity.
Qed.

author: xavierdpt

repo: research

save_path: github-repos/coq/xavierdpt-research


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

Require Import Orders BinInt Zcompare Zorder ZOrderedType
 GenericMinMax.

(** * Maximum and Minimum of two [Z] numbers *)

Local Open Scope Z_scope.

Unboxed Definition Zmax (n m:Z) :=
  match n ?= m with
    | Eq | Gt => n
    | Lt => m
  end.

Unboxed Definition Zmin (n m:Z) :=
  match n ?= m with
    | Eq | Lt => n
    | Gt => m
  end.

(** The functions [Zmax] and [Zmin] implement indeed
    a maximum and a minimum *)

Lemma Zmax_l : forall x y, y<=x -> Zmax x y = x.
Proof.
 unfold Zle, Zmax. intros x y. rewrite <- (Zcompare_antisym x y).
 destruct (x ?= y); intuition.
Qed.

Lemma Zmax_r : forall x y, x<=y -> Zmax x y = y.
Proof.
 unfold Zle, Zmax. intros x y. generalize (Zcompare_Eq_eq x y).
 destruct (x ?= y); intuition.
Qed.

Lemma Zmin_l : forall x y, x<=y -> Zmin x y = x.
Proof.
 unfold Zle, Zmin. intros x y. generalize (Zcompare_Eq_eq x y).
 destruct (x ?= y); intuition.
Qed.

Lemma Zmin_r : forall x y, y<=x -> Zmin x y = y.
Proof.
 unfold Zle, Zmin. intros x y.
 rewrite <- (Zcompare_antisym x y). generalize (Zcompare_Eq_eq x y).
 destruct (x ?= y); intuition.
Qed.

Module ZHasMinMax <: HasMinMax Z_as_OT.
 Definition max := Zmax.
 Definition min := Zmin.
 Definition max_l := Zmax_l.
 Definition max_r := Zmax_r.
 Definition min_l := Zmin_l.
 Definition min_r := Zmin_r.
End ZHasMinMax.

Module Z.

(** We obtain hence all the generic properties of max and min. *)

Include UsualMinMaxProperties Z_as_OT ZHasMinMax.

(** * Properties specific to the [Z] domain *)

(** Compatibilities (consequences of monotonicity) *)

Lemma plus_max_distr_l : forall n m p, Zmax (p + n) (p + m) = p + Zmax n m.
Proof.
 intros. apply max_monotone.
 intros x y. apply Zplus_le_compat_l.
Qed.

Lemma plus_max_distr_r : forall n m p, Zmax (n + p) (m + p) = Zmax n m + p.
Proof.
 intros. rewrite (Zplus_comm n p), (Zplus_comm m p), (Zplus_comm _ p).
 apply plus_max_distr_l.
Qed.

Lemma plus_min_distr_l : forall n m p, Zmin (p + n) (p + m) = p + Zmin n m.
Proof.
 intros. apply Z.min_monotone.
 intros x y. apply Zplus_le_compat_l.
Qed.

Lemma plus_min_distr_r : forall n m p, Zmin (n + p) (m + p) = Zmin n m + p.
Proof.
 intros. rewrite (Zplus_comm n p), (Zplus_comm m p), (Zplus_comm _ p).
 apply plus_min_distr_l.
Qed.

Lemma succ_max_distr : forall n m, Zsucc (Zmax n m) = Zmax (Zsucc n) (Zsucc m).
Proof.
 unfold Zsucc. intros. symmetry. apply plus_max_distr_r.
Qed.

Lemma succ_min_distr : forall n m, Zsucc (Zmin n m) = Zmin (Zsucc n) (Zsucc m).
Proof.
 unfold Zsucc. intros. symmetry. apply plus_min_distr_r.
Qed.

Lemma pred_max_distr : forall n m, Zpred (Zmax n m) = Zmax (Zpred n) (Zpred m).
Proof.
 unfold Zpred. intros. symmetry. apply plus_max_distr_r.
Qed.

Lemma pred_min_distr : forall n m, Zsucc (Zmin n m) = Zmin (Zsucc n) (Zsucc m).
Proof.
 unfold Zpred. intros. symmetry. apply plus_min_distr_r.
Qed.

(** Anti-monotonicity swaps the role of [min] and [max] *)

Lemma opp_max_distr : forall n m : Z, -(Zmax n m) = Zmin (- n) (- m).
Proof.
 intros. symmetry. apply min_max_antimonotone.
 intros x x'. red. red. rewrite <- Zcompare_opp; auto.
Qed.

Lemma opp_min_distr : forall n m : Z, - (Zmin n m) = Zmax (- n) (- m).
Proof.
 intros. symmetry. apply max_min_antimonotone.
 intros x x'. red. red. rewrite <- Zcompare_opp; auto.
Qed.

Lemma minus_max_distr_l : forall n m p, Zmax (p - n) (p - m) = p - Zmin n m.
Proof.
 unfold Zminus. intros. rewrite opp_min_distr. apply plus_max_distr_l.
Qed.

Lemma minus_max_distr_r : forall n m p, Zmax (n - p) (m - p) = Zmax n m - p.
Proof.
 unfold Zminus. intros. apply plus_max_distr_r.
Qed.

Lemma minus_min_distr_l : forall n m p, Zmin (p - n) (p - m) = p - Zmax n m.
Proof.
 unfold Zminus. intros. rewrite opp_max_distr. apply plus_min_distr_l.
Qed.

Lemma minus_min_distr_r : forall n m p, Zmin (n - p) (m - p) = Zmin n m - p.
Proof.
 unfold Zminus. intros. apply plus_min_distr_r.
Qed.

(** Compatibility with [Zpos] *)

Lemma pos_max : forall p q, Zpos (Pmax p q) = Zmax (Zpos p) (Zpos q).
Proof.
 intros; unfold Zmax, Pmax; simpl; generalize (Pcompare_Eq_eq p q).
 destruct Pcompare; auto.
 intro H; rewrite H; auto.
Qed.

Lemma pos_min : forall p q, Zpos (Pmin p q) = Zmin (Zpos p) (Zpos q).
Proof.
 intros; unfold Zmin, Pmin; simpl; generalize (Pcompare_Eq_eq p q).
 destruct Pcompare; auto.
Qed.

Lemma pos_max_1 : forall p, Zmax 1 (Zpos p) = Zpos p.
Proof.
  intros; unfold Zmax; simpl; destruct p; simpl; auto.
Qed.

Lemma pos_min_1 : forall p, Zmin 1 (Zpos p) = 1.
Proof.
  intros; unfold Zmax; simpl; destruct p; simpl; auto.
Qed.

End Z.

(** * Characterization of Pminus in term of Zminus and Zmax *)

Lemma Zpos_minus : forall p q, Zpos (Pminus p q) = Zmax 1 (Zpos p - Zpos q).
Proof.
  intros; simpl. destruct (Pcompare p q Eq) as [ ]_eqn:H.
  rewrite (Pcompare_Eq_eq _ _ H).
  unfold Pminus; rewrite Pminus_mask_diag; reflexivity.
  rewrite Pminus_Lt; auto.
  symmetry. apply Z.pos_max_1.
Qed.

(*begin hide*)
(* Compatibility with names of the old Zminmax file *)
Notation Zmin_max_absorption_r_r := Z.min_max_absorption (only parsing).
Notation Zmax_min_absorption_r_r := Z.max_min_absorption (only parsing).
Notation Zmax_min_distr_r := Z.max_min_distr (only parsing).
Notation Zmin_max_distr_r := Z.min_max_distr (only parsing).
Notation Zmax_min_modular_r := Z.max_min_modular (only parsing).
Notation Zmin_max_modular_r := Z.min_max_modular (only parsing).
Notation max_min_disassoc := Z.max_min_disassoc (only parsing).
(*end hide*)

author: JasonGross

repo: category-coq-experience-tests


text:
Require Import Coqlib.
Require Import ITreelib.
Require Import ImpPrelude.
Require Import STS.
Require Import Behavior.
Require Import ModSem.
Require Import Skeleton.
Require Import PCM.
Require Import Imp.
Require Import ImpNotations.

Set Implicit Arguments.

Section F.
  Context `{Σ: GRA.t}.

  Import ImpNotations.
  Local Open Scope expr_scope.
  Local Open Scope stmt_scope.

  Definition fF :=
    mk_function
      ["n"]
      ["g_ret"]
      (if# "n"
       then# "g_ret" =@ "g" ["n" - 1%Z : expr] ;#
             return# ("n" + "g_ret")
       else# return# 0%Z
       fi#).

  Definition f_prog : program :=
    mk_program
      "F"
      []
      [("g", 1)]
      []
      [("f", fF)]
  .

  Definition FSem ge: ModSem.t := ImpMod.modsem f_prog ge.
  Definition F : Mod.t := ImpMod.get_mod f_prog.

End F.

author: alxest

repo: CCR

save_path: github-repos/coq/alxest-CCR


text:
(* This used to raise an anomaly in 8.8 *)

Inductive T := Tau (t : T).

Notation idT t := (match t with Tau t => Tau t end).

Lemma match_itree : forall (t : T), t = idT t.
Proof. destruct t; auto. Qed.

Lemma what (k : unit -> T) : k tt = k tt.
Proof. rewrite match_itree. Abort.

author: princeton-vl

repo: CoqGym

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


text:
Require Import RelationClasses.
Require Import List.

From Paco Require Import paco.
From sflib Require Import sflib.

From PromisingLib Require Import Axioms.
From PromisingLib Require Import Basic.
From PromisingLib Require Import DataStructure.
From PromisingLib Require Import Language.
From PromisingLib Require Import Loc.
Require Import Time.
Require Import Event.
Require Import View.
Require Import Cell.
Require Import Memory.
Require Import MemoryFacts.
Require Import TView.
Require Import Local.
Require Import Thread.
Require Import Configuration.
Require Import Progress.
Require Import Behavior.
Require Import Cover.
Require Import PromiseConsistent.
Require Import Pred.
Require Import Trace.
Require Import JoinedView.

Require Import MemoryProps.
Require Import OrderedTimes.
Require SimMemory.

Require Import PFStep.
Require Import LocalPFThread.
Require Import TimeTraced.
Require Import PFConsistentStrong.
Require Import Mapping.
Require Import GoodFuture.
Require Import CapMap.
Require Import CapFlex.
Require Import Pred.

Require Import LocalPFSim.

Set Implicit Arguments.

Section SIMTIME.

  Variable L: Loc.t -> bool.
  Variable times: Loc.t -> Time.t -> Prop.
  Hypothesis WO: forall loc, well_ordered (times loc).
  Hypothesis INCR: forall nat loc, times loc (incr_time_seq nat).

  Lemma Forall2_tail A B (P: A -> B -> Prop) la lb a b
        (FORALL: List.Forall2 P (la ++ [a]) (lb ++ [b]))
    :
      List.Forall2 P la lb /\ P a b.
  Proof.
    eapply Forall2_app_inv_l in FORALL. des.
    inv FORALL0. inv H3. eapply app_inj_tail in FORALL1.
    des; clarify.
  Qed.

  Lemma promise_read_race views0 prom0 extra0 proml0
        c_src0 c_mid0 c_tgt0 c_tgt1 e tid tr_tgt tr_cert
        (STEPTGT: @times_configuration_step_strong times tr_tgt tr_cert e tid c_tgt0 c_tgt1)
        (SIM: sim_configuration L times (fun _ => True) views0 prom0 extra0 proml0 c_src0 c_mid0 c_tgt0)
        (READ: ~ List.Forall
                 (fun the => no_read_msgs
                               (all_promises (fun tid' => tid <> tid') prom0)
                               (snd the)) (tr_tgt ++ tr_cert))
        (WF_SRC: Configuration.wf c_src0)
        (PFSRC: PF.pf_configuration L c_src0)
        (WF_MID: JConfiguration.wf views0 c_mid0)
        (WF_TGT: Configuration.wf c_tgt0)
        (RACEFREE: ~ PFRace.multi_race L c_src0)
    :
      (<<UB: forall beh, behaviors (PFConfiguration.multi_step L) c_src0 beh>>).
  Proof.
    exploit times_configuration_step_future; eauto.
    { eapply times_configuration_step_strong_step; eauto. } i. des.
    exploit (@Memory.max_concrete_timemap_exists (Configuration.memory c_tgt1)); eauto.
    { eapply WF2. } intros [max MAX].
    eapply configuration_step_certify in STEPTGT; eauto. des.
    hexploit (@trace_times_list_exists (tr_tgt ++ tr_cert')). i. des.
    assert (exists (maxmap: TimeMap.t),
               (<<TIMES: forall loc' ts (IN: List.In ts (times0 loc')), Time.lt ts (maxmap loc')>>) /\
               (<<MAX: forall loc', Time.lt (Memory.max_ts loc' (Configuration.memory c_tgt0)) (maxmap loc')>>)).
    { hexploit (@choice
                  Loc.t
                  Time.t
                  (fun loc' max =>
                     (<<TIMES: forall ts (IN: List.In ts (times0 loc')), Time.lt ts (max)>>) /\
                     (<<MAX: Time.lt (Memory.max_ts loc' (Configuration.memory c_tgt0)) (max)>>))).
      { i. hexploit (finite_greatest (fun _ => True) (times0 x)). i. des.
        { exists (Time.incr (Time.join
                               (Memory.max_ts x (Configuration.memory c_tgt0))
                               to)).
          splits.
          { i. eapply GREATEST in IN0; auto. eapply TimeFacts.le_lt_lt; eauto.
            eapply TimeFacts.le_lt_lt.
            { eapply Time.join_r. }
            { eapply  Time.incr_spec. }
          }
          { eapply TimeFacts.le_lt_lt.
            { eapply Time.join_l. }
            { eapply  Time.incr_spec. }
          }
        }
        { exists (Time.incr (Memory.max_ts x (Configuration.memory c_tgt0))). splits.
          { i. eapply EMPTY in IN. ss. }
          { eapply Time.incr_spec. }
        }
      }
      i. des. exists f0. split.
      { ii. specialize (H loc'). des. auto. }
      { ii. specialize (H loc'). des. auto. }
    } i. des.

    assert (exists tid0 ploc pts rlc re pl0 pl1 tr0 tr1,
               (<<READING: PFRace.reading_event ploc pts re>>) /\
               (<<PROMISED: prom0 tid0 ploc pts>>) /\
               (<<NEQ: tid0 <> tid>>) /\
               (<<PROML: proml0 tid0 = pl0 ++ (ploc, pts) :: pl1>>) /\
               (<<TRACE: tr0 ++ (rlc, re) :: tr1 = tr_tgt ++ tr_cert'>>) /\
               (<<NOREAD: List.Forall (fun the => no_read_msgs
                                                    (all_promises (fun tid' => tid <> tid') prom0)
                                                    (snd the)) tr0>>)).
    { assert (FORALL: ~ Forall
                        (fun the => no_read_msgs (all_promises (fun tid' => tid <> tid') prom0) (snd the))
                        (tr_tgt ++ tr_cert')).
      { erewrite list_Forall_app in READ. erewrite list_Forall_app. ii.
        des. eapply READ. split; auto.
        eapply List.Forall_forall. ii. destruct STEPTGT0.
        - eapply list_Forall2_in2 in H0; eauto. des.
          erewrite List.Forall_forall in FORALL1. exploit (FORALL1 b); auto.
          i. destruct b, x. ss. unfold no_read_msgs in x1. inv SAT; ss.
          + ii. inv H0. eapply MAPIDENT in TO.
            { subst. eauto. }
            2: { refl. }
            eapply memory_future_concrete_promised.
            { eapply Memory.future_future_weak; eauto. }
            eapply sim_configuration_forget_tgt_concrete; eauto; ss.
          + ii. inv H0. eapply MAPIDENT in FROM.
            { subst. eauto. }
            2: { refl. }
            eapply memory_future_concrete_promised.
            { eapply Memory.future_future_weak; eauto. }
            eapply sim_configuration_forget_tgt_concrete; eauto; ss.
        - des. eapply list_Forall2_in2 in H0.
          2: { eapply List.in_or_app. left. eauto. } des.
          erewrite List.Forall_forall in FORALL1. exploit (FORALL1 b); auto.
          i. destruct b, x. ss. unfold no_read_msgs in x1. inv SAT; ss.
          + ii. inv H0. eapply MAPIDENT in TO.
            { subst. eauto. }
            2: { refl. }
            eapply memory_future_concrete_promised.
            { eapply Memory.future_future_weak; eauto. }
            eapply sim_configuration_forget_tgt_concrete; eauto; ss.
          + ii. inv H0. eapply MAPIDENT in FROM.
            { subst. eauto. }
            2: { refl. }
            eapply memory_future_concrete_promised.
            { eapply Memory.future_future_weak; eauto. }
            eapply sim_configuration_forget_tgt_concrete; eauto; ss.
      }
      exploit list_first_occurence. i. des.
      { exfalso. eapply FORALL; eauto. }
      destruct a as (rlc, re). ss.
      assert (exists ploc pts tid0, (<<PROMISED: prom0 tid0 ploc pts>>) /\ (<<READING: PFRace.reading_event ploc pts re>>) /\ (<<NEQ: tid <> tid0>>)).
      { eapply NNPP. ii. eapply FAIL. unfold no_read_msgs. ss. des_ifs.
        - ii. inv H0. eapply H; eauto. esplits; eauto. econs.
        - ii. inv H0. eapply H; eauto. esplits; eauto. econs. } des.
      assert (LIN: List.In (ploc, pts) (proml0 tid0)).
      { destruct (IdentMap.find tid0 (Configuration.threads c_tgt0)) as [[[lang_tgt st_tgt] lc_tgt]|] eqn:TIDTGT.
        { inv SIM. eapply CONSISTENT in TIDTGT; eauto.
          eapply (pi_consistent_promises TIDTGT) in PROMISED. auto. }
        { inv SIM. ss. specialize (THSJOIN tid0). specialize (THSPF tid0).
          unfold option_rel in THSJOIN.
          unfold option_rel in THSPF. des_ifs.
          eapply BOT in Heq1. des. exfalso. eapply PROM; eauto. }
      }
      eapply List.in_split in LIN. des. esplits; eauto.
    }
    des.

    exploit (@sim_configuration_certify_partial
               L times WO INCR
               (fun _ => True) tid0 ploc pts pl0 pl1); eauto.
    i. des. destruct x0; des.
    { ii. inv STEPSRC; ss. econs 3; eauto. econs; eauto. } exfalso.
    inv STEPSRC.
    2: { inv FINAL. } rename STEP0 into STEPSRC.

    hexploit times_configuration_opt_step_future; try apply STEPTGT; eauto. i. des.
    hexploit JConfiguration.opt_step_future; try apply STEPMID; eauto. i. des.
    hexploit PFConfiguration.step_trace_future; try apply STEPSRC; eauto. i. des.

    assert (IDENT: map_ident_in_memory (fun loc ts fts => ts = fts /\ Time.lt ts (maxmap loc))
                                       (Configuration.memory c_tgt0)).
    { ii. splits; auto. eapply TimeFacts.le_lt_lt; eauto. }
    assert (MAPLT0: mapping_map_lt (fun loc ts fts => ts = fts /\ Time.lt ts (maxmap loc))).
    { ii. des. subst. auto. }

    dup STEP. dep_inv STEP.
    exploit good_future_configuration_step_aux.
    { eauto. }
    { eapply STEP0. }
    { eauto. }
    { eapply WF0. }
    { inv SIM0. auto. }
    { eauto. }
    { erewrite <- TID.
      inv STEPTGT; auto. inv STEP; auto.
      ss. erewrite IdentMap.gso; eauto.
    }
    { eapply map_ident_in_memory_local; eauto.
      { eapply WF_TGT; eauto. }
      { eapply WF_TGT; eauto. }
    }
    { eapply max_good_future_map; eauto. eapply WF_TGT. }
    { eauto. }
    { eapply map_ident_in_memory_closed_timemap; eauto. eapply WF_TGT. }
    { erewrite SC. refl. }
    { erewrite app_nil_r.
      eapply List.Forall_impl; try apply WFTIME; eauto. i. ss.
      eapply wf_time_evt_mon; eauto. i. ss. eauto. }
    i. des. ss.

    inv STEP. guardH CERTBOT0.
    hexploit sim_configuration_sim_thread; eauto. i. des.
    generalize (sim_configuration_forget_exclusive SIM0 WF3 TIDSRC).
    intros EXCLUSIVE.
    generalize (sim_configuration_extra_exclusive SIM0 WF3 TIDSRC).
    intros EXCLUSIVEEXTRA.

    eapply Forall_app_inv in TIMES1. des.
    exploit Trace.steps_future.
    { eapply STEPS0. }
    { eapply WF0; eauto. }
    { eapply WF0; eauto. }
    { eapply WF0; eauto. } i. ss. des.
    exploit Thread.step_future; eauto. i. des. ss. ss.

    assert (exists tr_read rlc' re' th,
               (<<STEPS: Trace.steps (tr_read ++ [(rlc', re')]) (Thread.mk _ st0 lc0 (Configuration.sc c_tgt2) (Configuration.memory c_tgt2)) th>>) /\
               (<<REST: exists tr_rest,
                   Trace.steps tr_rest th (Thread.mk _ st2 lc2 sc0 memory0)>>) /\
               (<<READING: PFRace.reading_event ploc pts re'>>) /\
               (<<SILENT: Forall (fun the => ThreadEvent.get_machine_event (snd the) = MachineEvent.silent) (tr_read ++ [(rlc', re')])>>) /\
               (<<WFTIME: Forall (fun the => wf_time_evt times (snd the)) (tr_read ++ [(rlc', re')])>>) /\
               (<<NOREAD: Forall (fun the => no_read_msgs (all_promises (fun tid' => tid <> tid') (fun tid' => if Ident.eq_dec tid' tid0 then prom_self else prom0 tid')) (snd the)) (tr_read ++ [(rlc', re')])>>)).
    { assert (NOREAD0: Forall (fun the => no_read_msgs (all_promises (fun tid' => tid <> tid') (fun tid' => if Ident.eq_dec tid' tid0 then prom_self else prom0 tid')) (snd the)) tr0).
      { eapply Forall_impl; try apply NOREAD; eauto. i. ss.
        eapply no_read_msgs_mon; [eauto|]. i. inv PR.
        econs; eauto. des_ifs. eapply DECR; eauto. }
      assert (NOREAD1: no_read_msgs (all_promises (fun tid' => tid <> tid') (fun tid' => if Ident.eq_dec tid' tid0 then prom_self else prom0 tid')) re).
      { assert (NPROM: ~ (all_promises (fun tid' => tid <> tid') (fun tid' => if Ident.eq_dec tid' tid0 then prom_self else prom0 tid')) ploc pts).
        { ii. inv H. des_ifs.
          { eapply (WRITTEN ploc pts); eauto.
            eapply List.in_or_app. right. ss. auto. }
          { clear - n WF_SRC SIM PROMS PROMISED.
            dup SIM. inv SIM. specialize (THSPF tid0).
            unfold option_rel in *. des_ifs.
            { inv THSPF. inv LOCAL. destruct st as [lang st].
              exploit sim_configuration_forget_exclusive; try eassumption.
              { econs; eauto. }
              i. des. ss. inv UNCH.
              set (PROM := (sim_promise_contents PROMS0) ploc pts).
              rewrite NPROM in *. inv PROM; try by (eapply NPROM0; eauto).
            }
            { eapply BOT in Heq. des. eapply PROM; eauto. }
          }
        }
        { inv READING; eauto. }
      }

      erewrite <- TRACE in *.
      hexploit (list_match_rev tr1). i. des; clarify.
      { eapply Forall2_tail in TRACE1. des. ss.
        exists tr'0, (Thread.local e3), e1, (Thread.mk _ st2 lc2 sc0 memory0). splits.
        { eapply Trace.steps_trans; eauto. }
        { eauto. }
        { inv READING; inv EVT; econs; eauto. }
        { eapply Forall_app; eauto. econs; eauto. ss.
          inv READING; inv EVT; eauto. }
        { eapply Forall_app; eauto. }
        { eapply Forall_app.
          { eapply Forall_forall. i.
            eapply list_Forall2_in in TRACE1; eauto. des.
            eapply Forall_forall in IN; try apply NOREAD0. ss.
            destruct a, x. ss. inv EVT0; ss. }
          { econs; eauto. ss. clear - NOREAD1 EVT. inv EVT; ss. }
        }
      }
      { rewrite app_comm_cons in *. rewrite app_assoc in TRACE1.
        eapply Forall2_tail in TRACE1. des. ss.
        replace (tr0 ++ (rlc, re) :: tl_rev) with ((tr0 ++ [(rlc, re)]) ++ tl_rev) in *.
        2: { erewrite <- app_assoc. auto. }
        eapply Forall2_app_inv_l in TRACE1. des. clarify.
        eapply Forall2_app_inv_l in TRACE1. des. clarify.
        inv TRACE3. inv H4. destruct y. des. ss.
        eapply Trace.steps_separate in STEPS0. des.
        exists l1'0, t, t0, th1. splits.
        { eauto. }
        { esplits. eapply Trace.steps_trans; eauto. }
        { inv READING; inv EVT0; econs; eauto. }
        { eapply Forall_app_inv in SILENT0. des. auto. }
        { eapply Forall_app_inv in FORALL1. des. auto. }
        { eapply Forall_app.
          { eapply Forall_forall. i.
            eapply list_Forall2_in in TRACE1; eauto. des.
            eapply Forall_forall in IN; try apply NOREAD0. ss.
            destruct a, x. ss. clear - IN EVT1. inv EVT1; ss. }
          { econs; eauto. ss. clear - NOREAD1 EVT0. inv EVT0; ss. }
        }
      }
    } des.

    exploit Trace.steps_future; try apply STEPS1; ss.
    { eapply WF0; eauto. }
    { eapply WF0; eauto. }
    { eapply WF0; eauto. } i. des.

    assert (CONSISTENT1: Local.promise_consistent (Thread.local th)).
    { exploit Trace.steps_future; try apply REST; eauto. i. des. ss.
      eapply Trace.steps_promise_consistent; eauto. ss.
      destruct (classic (e1 = ThreadEvent.failure)) as [EQ0|NEQ0].
      { subst. inv STEP2; inv STEP. ss. inv LOCAL. inv LOCAL0. auto. }
      specialize (CONSISTENT0 NEQ0).
      eapply pf_consistent_super_strong_consistent in CONSISTENT0; eauto.
      eapply consistent_promise_consistent in CONSISTENT0; eauto.
    }

    hexploit sim_configuration_sim_thread; eauto. i. des.
    hexploit sim_thread_steps_silent; try apply STEPS1; eauto.
    { eapply Forall_forall. i. splits.
      - eapply Forall_forall in WFTIME0; eauto.
      - eapply Forall_forall in NOREAD0; eauto.
      - eapply Forall_forall in SILENT1; eauto. }
    { eapply WF3. }
    { eapply WF1. }
    { eapply WF0. }
    { eapply WF3. }
    { eapply WF1. }
    { eapply WF0. }
    { eapply WF3; eauto. }
    { eapply WF1; eauto. }
    { eapply WF0; eauto. }
    { inv SIM0. ss. }
    { inv SIM0. ss. }

    { eapply sim_configuration_forget_exclusive; eauto. }
    { eapply sim_configuration_extra_exclusive; eauto. }
    { inv SIM0. ss. }
    { eapply WF1; eauto. }
    { eapply WF1; eauto. }
    { eapply WF1; eauto. } i. des.

    exploit sim_traces_sim_event_exists.
    { eauto. }
    { eauto. }
    { eapply List.in_or_app. right. ss. eauto. }
    { ii. subst. inv READING0. }
    { inv READING0; ss. } i. des.
    eapply in_split in IN. des. subst.
    eapply Trace.steps_separate in STEPSRC0. des.
    inv STEPS3; clarify.

    exploit Trace.steps_future; try apply STEPS2; eauto.
    { eapply WF3; eauto. }
    { eapply WF3; eauto. }
    { eapply WF3; eauto. } i. des. ss.
    exploit Thread.step_future; eauto. i. des.

    eapply RACEFREE. econs.
    { eauto. }
    { eauto. }
    { eauto. }
    { eauto. }
    { eauto. }
    { eapply sim_traces_pf in TRACE2; eauto.
      eapply Forall_app_inv in TRACE2. des. auto. }
    { eapply step_promise_consistent in STEP; eauto.
      eapply Trace.steps_promise_consistent in STEPS4; eauto.
      dep_inv THREAD.
      eapply sim_local_strong_sim_local in LOCALPF.
      eapply JSim.sim_local_promise_consistent in LOCALJOIN; eauto.
      eapply sim_promise_consistent; eauto.
    }
    { eauto. }
    { clear - EVENT READING0. inv READING0; inv EVENT; econs. }
    { exploit sim_configuration_forget_tgt_concrete; try apply SIM; eauto; ss.
      i. des; auto. }
  Qed.
End SIMTIME.

author: snu-sf

repo: promising-ldrf-coq


text:
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2015   --   INRIA - CNRS - Paris-Sud University  *)
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)

(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below    *)
Require Import BuiltIn.
Require BuiltIn.

(* Why3 goal *)
Lemma andb_def : forall (x:bool) (y:bool),
  ((Init.Datatypes.andb x y) = match x with
  | true => y
  | false => false
  end).
Proof.
intros x y.
apply refl_equal.
Qed.

(* Why3 goal *)
Lemma orb_def : forall (x:bool) (y:bool),
  ((Init.Datatypes.orb x y) = match x with
  | false => y
  | true => true
  end).
Proof.
intros x y.
apply refl_equal.
Qed.

(* Why3 goal *)
Lemma notb_def : forall (x:bool),
  ((Init.Datatypes.negb x) = match x with
  | false => true
  | true => false
  end).
Proof.
intros x.
apply refl_equal.
Qed.

(* Why3 goal *)
Lemma xorb_def : forall (x:bool) (y:bool),
  ((Init.Datatypes.xorb x y) = match x with
  | false => y
  | true => (Init.Datatypes.negb y)
  end).
Proof.
intros x y.
destruct x; destruct y; auto.
Qed.

(* Why3 goal *)
Lemma implb_def : forall (x:bool) (y:bool),
  ((Init.Datatypes.implb x y) = match x with
  | false => true
  | true => y
  end).
Proof.
now intros [|] [|].
Qed.

author: ssaavedra


text:
(** Camera of discardable fractions.

    This is a generalisation of the fractional camera where elements can
    represent both ownership of a fraction (as in the fractional camera) and the
    knowledge that a fraction has been discarded.

    Ownership of a fraction is denoted [DfracOwn q] and behaves identically to
    [q] of the fractional camera.

    Knowledge that a fraction has been discarded is denoted [DfracDiscarded].
    This elements is its own core, making ownership persistent.

    One can make a frame preserving update from _owning_ a fraction to _knowing_
    that the fraction has been discarded.

    Crucially, ownership over 1 is an exclusive element just as it is in the
    fractional camera. Hence owning 1 implies that no fraction has been
    discarded. Conversely, knowing that a fraction has been discarded implies
    that no one can own 1. And, since discarding is an irreversible operation,
    it also implies that no one can own 1 in the future *)
From stdpp Require Import countable.
From iris.algebra Require Export cmra.
From iris.algebra Require Import proofmode_classes updates frac.
From iris.prelude Require Import options.

(** An element of dfrac denotes ownership of a fraction, knowledge that a
    fraction has been discarded, or both. Note that [DfracBoth] can be written
    as [DfracOwn q ⋅ DfracDiscarded]. This should be used instead
    of [DfracBoth] which is for internal use only. *)
Inductive dfrac :=
  | DfracOwn : Qp → dfrac
  | DfracDiscarded : dfrac
  | DfracBoth : Qp → dfrac.

(* This notation is intended to be used as a component in other notations that
   include discardable fractions. The notation provides shorthands for the
   constructors and the commonly used full fraction. For an example
   demonstrating how this can be used see the notation in [gen_heap.v]. *)
Declare Custom Entry dfrac.
Notation "{ dq }" := (dq) (in custom dfrac at level 1, dq constr).
Notation "□" := DfracDiscarded (in custom dfrac).
Notation "{# q }" := (DfracOwn q) (in custom dfrac at level 1, q constr).
Notation "" := (DfracOwn 1) (in custom dfrac).

Section dfrac.
  Canonical Structure dfracO := leibnizO dfrac.

  Implicit Types p q : Qp.
  Implicit Types dp dq : dfrac.

  Global Instance dfrac_inhabited : Inhabited dfrac := populate DfracDiscarded.
  Global Instance dfrac_eq_dec : EqDecision dfrac.
  Proof. solve_decision. Defined.
  Global Instance dfrac_countable : Countable dfrac.
  Proof.
    set (enc dq := match dq with
      | DfracOwn q => inl q
      | DfracDiscarded => inr (inl ())
      | DfracBoth q => inr (inr q)
      end).
    set (dec y := Some match y with
      | inl q => DfracOwn q
      | inr (inl ()) => DfracDiscarded
      | inr (inr q) => DfracBoth q
      end).
    refine (inj_countable enc dec _). by intros [].
  Qed.

  Global Instance DfracOwn_inj : Inj (=) (=) DfracOwn.
  Proof. by injection 1. Qed.
  Global Instance DfracBoth_inj : Inj (=) (=) DfracBoth.
  Proof. by injection 1. Qed.

  (** An element is valid as long as the sum of its content is less than one. *)
  Local Instance dfrac_valid_instance : Valid dfrac := λ dq,
    match dq with
    | DfracOwn q => q ≤ 1
    | DfracDiscarded => True
    | DfracBoth q => q < 1
    end%Qp.

  (** As in the fractional camera the core is undefined for elements denoting
     ownership of a fraction. For elements denoting the knowledge that a fraction has
     been discarded the core is the identity function. *)
  Local Instance dfrac_pcore_instance : PCore dfrac := λ dq,
    match dq with
    | DfracOwn q => None
    | DfracDiscarded => Some DfracDiscarded
    | DfracBoth q => Some DfracDiscarded
    end.

  (** When elements are combined, ownership is added together and knowledge of
     discarded fractions is combined with the max operation. *)
  Local Instance dfrac_op_instance : Op dfrac := λ dq dp,
    match dq, dp with
    | DfracOwn q, DfracOwn q' => DfracOwn (q + q')
    | DfracOwn q, DfracDiscarded => DfracBoth q
    | DfracOwn q, DfracBoth q' => DfracBoth (q + q')
    | DfracDiscarded, DfracOwn q' => DfracBoth q'
    | DfracDiscarded, DfracDiscarded => DfracDiscarded
    | DfracDiscarded, DfracBoth q' => DfracBoth q'
    | DfracBoth q, DfracOwn q' => DfracBoth (q + q')
    | DfracBoth q, DfracDiscarded => DfracBoth q
    | DfracBoth q, DfracBoth q' => DfracBoth (q + q')
    end.

  Lemma dfrac_op_own q p : DfracOwn p ⋅ DfracOwn q = DfracOwn (p + q).
  Proof. done. Qed.

  Lemma dfrac_op_discarded :
    DfracDiscarded ⋅ DfracDiscarded = DfracDiscarded.
  Proof. done. Qed.

  Lemma dfrac_own_included q p : DfracOwn q ≼ DfracOwn p ↔ (q < p)%Qp.
  Proof.
    rewrite Qp.lt_sum. split.
    - rewrite /included /op /dfrac_op_instance. intros [[o| |?] [= ->]]. by exists o.
    - intros [o ->]. exists (DfracOwn o). by rewrite dfrac_op_own.
  Qed.

  (* [dfrac] does not have a unit so reflexivity is not for granted! *)
  Lemma dfrac_discarded_included :
    DfracDiscarded ≼ DfracDiscarded.
  Proof. exists DfracDiscarded. done. Qed.

  Definition dfrac_ra_mixin : RAMixin dfrac.
  Proof.
    split; try apply _.
    - intros [?| |?] ? dq <-; intros [= <-]; eexists _; done.
    - intros [?| |?] [?| |?] [?| |?];
        rewrite /op /dfrac_op_instance 1?assoc_L 1?assoc_L; done.
    - intros [?| |?] [?| |?];
        rewrite /op /dfrac_op_instance 1?(comm_L Qp.add); done.
    - intros [?| |?] dq; rewrite /pcore /dfrac_pcore_instance; intros [= <-];
        rewrite /op /dfrac_op_instance; done.
    - intros [?| |?] ? [= <-]; done.
    - intros [?| |?] [?| |?] ? [[?| |?] [=]] [= <-]; eexists _; split; try done;
        apply dfrac_discarded_included.
    - intros [q| |q] [q'| |q']; rewrite /op /dfrac_op_instance /valid /dfrac_valid_instance //.
      + intros. trans (q + q')%Qp; [|done]. apply Qp.le_add_l.
      + apply Qp.lt_le_incl.
      + intros. trans (q + q')%Qp; [|by apply Qp.lt_le_incl]. apply Qp.le_add_l.
      + intros. trans (q + q')%Qp; [|done]. apply Qp.lt_add_l.
      + intros. trans (q + q')%Qp; [|done]. apply Qp.lt_add_l.
  Qed.
  Canonical Structure dfracR := discreteR dfrac dfrac_ra_mixin.

  Global Instance dfrac_cmra_discrete : CmraDiscrete dfracR.
  Proof. apply discrete_cmra_discrete. Qed.

  Global Instance dfrac_full_exclusive : Exclusive (DfracOwn 1).
  Proof.
    intros [q| |q];
      rewrite /op /cmra_op -cmra_discrete_valid_iff /valid /cmra_valid //=.
    - apply Qp.not_add_le_l.
    - move=> /Qp.lt_le_incl. apply Qp.not_add_le_l.
  Qed.

  Global Instance dfrac_cancelable q : Cancelable (DfracOwn q).
  Proof.
    apply: discrete_cancelable.
    intros [q1| |q1][q2| |q2] _ [=]; simplify_eq/=; try done.
    - by destruct (Qp.add_id_free q q2).
    - by destruct (Qp.add_id_free q q1).
  Qed.
  Global Instance dfrac_own_id_free q : IdFree (DfracOwn q).
  Proof. intros [q'| |q'] _ [=]. by apply (Qp.add_id_free q q'). Qed.
  Global Instance dfrac_discarded_core_id : CoreId DfracDiscarded.
  Proof. by constructor. Qed.

  Lemma dfrac_valid_own p : ✓ DfracOwn p ↔ (p ≤ 1)%Qp.
  Proof. done. Qed.
  Lemma dfrac_valid_own_1 : ✓ DfracOwn 1.
  Proof. done. Qed.

  Lemma dfrac_valid_own_r dq q : ✓ (dq ⋅ DfracOwn q) → (q < 1)%Qp.
  Proof.
    destruct dq as [q'| |q']; [|done|].
    - apply Qp.lt_le_trans, Qp.lt_add_r.
    - intro Hlt. etrans; last apply Hlt. apply Qp.lt_add_r.
  Qed.

  Lemma dfrac_valid_own_l dq q : ✓ (DfracOwn q ⋅ dq) → (q < 1)%Qp.
  Proof. rewrite comm. apply dfrac_valid_own_r. Qed.

  Lemma dfrac_valid_discarded : ✓ DfracDiscarded.
  Proof. done. Qed.

  Lemma dfrac_valid_own_discarded q :
    ✓ (DfracOwn q ⋅ DfracDiscarded) ↔ (q < 1)%Qp.
  Proof. done. Qed.

  Global Instance dfrac_is_op q q1 q2 :
    IsOp q q1 q2 →
    IsOp' (DfracOwn q) (DfracOwn q1) (DfracOwn q2).
  Proof. rewrite /IsOp' /IsOp dfrac_op_own=>-> //. Qed.

  (** Discarding a fraction is a frame preserving update. *)
  Lemma dfrac_discard_update dq : dq ~~> DfracDiscarded.
  Proof.
    intros n [[q'| |q']|]; rewrite -!cmra_discrete_valid_iff //=.
    - apply dfrac_valid_own_r.
    - apply cmra_valid_op_r.
  Qed.

End dfrac.

author: amintimany

repo: iris

save_path: github-repos/coq/amintimany-iris


text:
(** * Prop: Propositions and Evidence *)

Require Export Logic.
Require Import Basics.
Require Import Induction.

(* ####################################################### *)
(** * From Boolean Functions to Propositions *)

(** In chapter [Basics] we defined a _function_ [evenb] that tests a
    number for evenness, yielding [true] if so.  We can use this
    function to define the _proposition_ that some number [n] is
    even: *)

Definition even (n:nat) : Prop :=
  evenb n = true.

(** That is, we can define "[n] is even" to mean "the function [evenb]
    returns [true] when applied to [n]."

    Note that here we have given a name
    to a proposition using a [Definition], just as we have
    given names to expressions of other sorts. This isn't a fundamentally
    new kind of proposition;  it is still just an equality. *)

(** Another alternative is to define the concept of evenness
    directly.  Instead of going via the [evenb] function ("a number is
    even if a certain computation yields [true]"), we can say what the
    concept of evenness means by giving two different ways of
    presenting _evidence_ that a number is even. *)

(** * Inductively Defined Propositions *)

Inductive ev : nat -> Prop :=
  | ev_0 : ev O
  | ev_SS : forall n:nat, ev n -> ev (S (S n)).

(** This definition says that there are two ways to give
    evidence that a number [m] is even.  First, [0] is even, and
    [ev_0] is evidence for this.  Second, if [m = S (S n)] for some
    [n] and we can give evidence [e] that [n] is even, then [m] is
    also even, and [ev_SS n e] is the evidence. *)

(** **** Exercise: 1 star (double_even) *)

Theorem double_even : forall n,
  ev (double n).
Proof.
  intros.
  induction n.
  compute.
  apply ev_0.
  compute.
  apply ev_SS.
  apply IHn.
Qed.

(** *** Discussion: Computational vs. Inductive Definitions *)

(** We have seen that the proposition "[n] is even" can be
    phrased in two different ways -- indirectly, via a boolean testing
    function [evenb], or directly, by inductively describing what
    constitutes evidence for evenness.  These two ways of defining
    evenness are about equally easy to state and work with.  Which we
    choose is basically a question of taste.

    However, for many other properties of interest, the direct
    inductive definition is preferable, since writing a testing
    function may be awkward or even impossible.

    One such property is [beautiful].  This is a perfectly sensible
    definition of a set of numbers, but we cannot translate its
    definition directly into a Coq Fixpoint (or into a recursive
    function in any other common programming language).  We might be
    able to find a clever way of testing this property using a
    [Fixpoint] (indeed, it is not too hard to find one in this case),
    but in general this could require arbitrarily deep thinking.  In
    fact, if the property we are interested in is uncomputable, then
    we cannot define it as a [Fixpoint] no matter how hard we try,
    because Coq requires that all [Fixpoint]s correspond to
    terminating computations.

    On the other hand, writing an inductive definition of what it
    means to give evidence for the property [beautiful] is
    straightforward. *)

(** **** Exercise: 1 star (ev__even) *)
(** Here is a proof that the inductive definition of evenness implies
    the computational one. *)

Theorem ev__even : forall n,
  ev n -> even n.
Proof.
  intros n E. induction E as [| n' E'].
  Case "E = ev_0".
    unfold even. reflexivity.
  Case "E = ev_SS n' E'".
    unfold even. apply IHE'.
Qed.

(** Could this proof also be carried out by induction on [n] instead
    of [E]?  If not, why not? *)

Goal forall n, ev n -> even n.
Proof.
  intros n E.
  induction n.
  unfold even. reflexivity.
  unfold even.  rewrite <-  IHn.
  Abort.

 (* FILL IN HERE *)
(** [] *)

(** The induction principle for inductively defined propositions does
    not follow quite the same form as that of inductively defined
    sets.  For now, you can take the intuitive view that induction on
    evidence [ev n] is similar to induction on [n], but restricts our
    attention to only those numbers for which evidence [ev n] could be
    generated.  We'll look at the induction principle of [ev] in more
    depth below, to explain what's really going on. *)

(** **** Exercise: 1 star (l_fails) *)
(** The following proof attempt will not succeed.
     Theorem l : forall n,
       ev n.
     Proof.
       intros n. induction n.
         Case "O". simpl. apply ev_0.
         Case "S".
           ...
   Intuitively, we expect the proof to fail because not every
   number is even. However, what exactly causes the proof to fail?

(* FILL IN HERE *)
*)
(** [] *)

(** **** Exercise: 2 stars (ev_sum) *)
(** Here's another exercise requiring induction. *)

Theorem ev_sum : forall n m,
   ev n -> ev m -> ev (n+m).
Proof.
  (* FILL IN HERE *) Admitted.
(** [] *)

(* ##################################################### *)
(** ** Example *)

(**  As a running example, let's
    define a simple property of natural numbers -- we'll call it
    "[beautiful]." *)

(** Informally, a number is [beautiful] if it is [0], [3], [5], or the
    sum of two [beautiful] numbers.

    More pedantically, we can define [beautiful] numbers by giving four
    rules:

       - Rule [b_0]: The number [0] is [beautiful].
       - Rule [b_3]: The number [3] is [beautiful].
       - Rule [b_5]: The number [5] is [beautiful].
       - Rule [b_sum]: If [n] and [m] are both [beautiful], then so is
         their sum. *)
(** ** Inference Rules *)
(** We will see many definitions like this one during the rest
    of the course, and for purposes of informal discussions, it is
    helpful to have a lightweight notation that makes them easy to
    read and write.  _Inference rules_ are one such notation: *)
(**
                              -----------                               (b_0)
                              beautiful 0

                              ------------                              (b_3)
                              beautiful 3

                              ------------                              (b_5)
                              beautiful 5

                       beautiful n     beautiful m
                       ---------------------------                      (b_sum)
                              beautiful (n+m)
*)

(** *** *)
(** Each of the textual rules above is reformatted here as an
    inference rule; the intended reading is that, if the _premises_
    above the line all hold, then the _conclusion_ below the line
    follows.  For example, the rule [b_sum] says that, if [n] and [m]
    are both [beautiful] numbers, then it follows that [n+m] is
    [beautiful] too.  If a rule has no premises above the line, then
    its conclusion holds unconditionally.

    These rules _define_ the property [beautiful].  That is, if we
    want to convince someone that some particular number is [beautiful],
    our argument must be based on these rules.  For a simple example,
    suppose we claim that the number [5] is [beautiful].  To support
    this claim, we just need to point out that rule [b_5] says so.
    Or, if we want to claim that [8] is [beautiful], we can support our
    claim by first observing that [3] and [5] are both [beautiful] (by
    rules [b_3] and [b_5]) and then pointing out that their sum, [8],
    is therefore [beautiful] by rule [b_sum].  This argument can be
    expressed graphically with the following _proof tree_: *)
(**
         ----------- (b_3)   ----------- (b_5)
         beautiful 3         beautiful 5
         ------------------------------- (b_sum)
                   beautiful 8
*)
(** *** *)
(**
    Of course, there are other ways of using these rules to argue that
    [8] is [beautiful], for instance:
         ----------- (b_5)   ----------- (b_3)
         beautiful 5         beautiful 3
         ------------------------------- (b_sum)
                   beautiful 8
*)

(** **** Exercise: 1 star (varieties_of_beauty) *)
(** How many different ways are there to show that [8] is [beautiful]? *)

(* FILL IN HERE *)
(** [] *)

(** *** *)
(** In Coq, we can express the definition of [beautiful] as
    follows: *)

Inductive beautiful : nat -> Prop :=
  b_0   : beautiful 0
| b_3   : beautiful 3
| b_5   : beautiful 5
| b_sum : forall n m, beautiful n -> beautiful m -> beautiful (n+m).

(** The first line declares that [beautiful] is a proposition -- or,
    more formally, a family of propositions "indexed by" natural
    numbers.  (That is, for each number [n], the claim that "[n] is
    [beautiful]" is a proposition.)  Such a family of propositions is
    often called a _property_ of numbers.  Each of the remaining lines
    embodies one of the rules for [beautiful] numbers.
*)
(** *** *)
(**
    The rules introduced this way have the same status as proven
    theorems; that is, they are true axiomatically.
    So we can use Coq's [apply] tactic with the rule names to prove
    that particular numbers are [beautiful].  *)

Theorem three_is_beautiful: beautiful 3.
Proof.
   (* This simply follows from the rule [b_3]. *)
   apply b_3.
Qed.

Theorem eight_is_beautiful: beautiful 8.
Proof.
   (* First we use the rule [b_sum], telling Coq how to
      instantiate [n] and [m]. *)
   apply b_sum with (n:=3) (m:=5).
   (* To solve the subgoals generated by [b_sum], we must provide
      evidence of [beautiful 3] and [beautiful 5]. Fortunately we
      have rules for both. *)
   apply b_3.
   apply b_5.
Qed.

(** *** *)
(** As you would expect, we can also prove theorems that have
hypotheses about [beautiful]. *)

Theorem beautiful_plus_eight: forall n, beautiful n -> beautiful (8+n).
Proof.
  intros n B.
  apply b_sum with (n:=8) (m:=n).
  apply eight_is_beautiful.
  apply B.
Qed.

(** **** Exercise: 2 stars (b_times2) *)
Theorem b_times2: forall n, beautiful n -> beautiful (2*n).
Proof.
    (* FILL IN HERE *) Admitted.
(** [] *)

(** **** Exercise: 3 stars (b_timesm) *)
Theorem b_timesm: forall n m, beautiful n -> beautiful (m*n).
Proof.
   (* FILL IN HERE *) Admitted.
(** [] *)

(* ####################################################### *)
(** ** Induction Over Evidence *)

(** Besides _constructing_ evidence that numbers are beautiful, we can
    also _reason about_ such evidence. *)

(** The fact that we introduced [beautiful] with an [Inductive]
    declaration tells Coq not only that the constructors [b_0], [b_3],
    [b_5] and [b_sum] are ways to build evidence, but also that these
    four constructors are the _only_ ways to build evidence that
    numbers are beautiful. *)

(** In other words, if someone gives us evidence [E] for the assertion
    [beautiful n], then we know that [E] must have one of four shapes:

      - [E] is [b_0] (and [n] is [O]),
      - [E] is [b_3] (and [n] is [3]),
      - [E] is [b_5] (and [n] is [5]), or
      - [E] is [b_sum n1 n2 E1 E2] (and [n] is [n1+n2], where [E1] is
        evidence that [n1] is beautiful and [E2] is evidence that [n2]
        is beautiful). *)

(** *** *)
(** This permits us to _analyze_ any hypothesis of the form [beautiful
    n] to see how it was constructed, using the tactics we already
    know.  In particular, we can use the [induction] tactic that we
    have already seen for reasoning about inductively defined _data_
    to reason about inductively defined _evidence_.

    To illustrate this, let's define another property of numbers: *)

Inductive gorgeous : nat -> Prop :=
  g_0 : gorgeous 0
| g_plus3 : forall n, gorgeous n -> gorgeous (3+n)
| g_plus5 : forall n, gorgeous n -> gorgeous (5+n).

(** **** Exercise: 1 star (gorgeous_tree) *)
(** Write out the definition of [gorgeous] numbers using inference rule
    notation.

(* FILL IN HERE *)
[]
*)

(** **** Exercise: 1 star (gorgeous_plus13) *)
Theorem gorgeous_plus13: forall n,
  gorgeous n -> gorgeous (13+n).
Proof.
   (* FILL IN HERE *) Admitted.
(** [] *)

(** *** *)
(** It seems intuitively obvious that, although [gorgeous] and
    [beautiful] are presented using slightly different rules, they are
    actually the same property in the sense that they are true of the
    same numbers.  Indeed, we can prove this. *)

Theorem gorgeous__beautiful : forall n,
  gorgeous n -> beautiful n.
Proof.
   intros n H.
   induction H as [|n'|n'].
   Case "g_0".
       apply b_0.
   Case "g_plus3".
       apply b_sum. apply b_3.
       apply IHgorgeous.
   Case "g_plus5".
       apply b_sum. apply b_5. apply IHgorgeous.
Qed.

(** Notice that the argument proceeds by induction on the _evidence_ [H]! *)

(** Let's see what happens if we try to prove this by induction on [n]
   instead of induction on the evidence [H]. *)

Theorem gorgeous__beautiful_FAILED : forall n,
  gorgeous n -> beautiful n.
Proof.
   intros. induction n as [| n'].
   Case "n = 0". apply b_0.
   Case "n = S n'". (* We are stuck! *)
Abort.

(** The problem here is that doing induction on [n] doesn't yield a
    useful induction hypothesis. Knowing how the property we are
    interested in behaves on the predecessor of [n] doesn't help us
    prove that it holds for [n]. Instead, we would like to be able to
    have induction hypotheses that mention other numbers, such as [n -
    3] and [n - 5]. This is given precisely by the shape of the
    constructors for [gorgeous]. *)

(** **** Exercise: 2 stars (gorgeous_sum) *)
Theorem gorgeous_sum : forall n m,
  gorgeous n -> gorgeous m -> gorgeous (n + m).
Proof.
 (* FILL IN HERE *) Admitted.
(** [] *)

(** **** Exercise: 3 stars, advanced (beautiful__gorgeous) *)
Theorem beautiful__gorgeous : forall n, beautiful n -> gorgeous n.
Proof.
 (* FILL IN HERE *) Admitted.
(** [] *)

(** **** Exercise: 3 stars, optional (g_times2) *)
(** Prove the [g_times2] theorem below without using [gorgeous__beautiful].
    You might find the following helper lemma useful. *)

Lemma helper_g_times2 : forall x y z, x + (z + y)= z + x + y.
Proof.
   (* FILL IN HERE *) Admitted.

Theorem g_times2: forall n, gorgeous n -> gorgeous (2*n).
Proof.
   intros n H. simpl.
   induction H.
   (* FILL IN HERE *) Admitted.
(** [] *)

(* ####################################################### *)
(** ** [Inversion] on Evidence *)

(** Another situation where we want to analyze evidence for evenness
    is when proving that, if [n] is even, then [pred (pred n)] is
    too.  In this case, we don't need to do an inductive proof.  The
    right tactic turns out to be [inversion].  *)

Theorem ev_minus2: forall n,
  ev n -> ev (pred (pred n)).
Proof.
  intros n E.
  inversion E as [| n' E'].
  Case "E = ev_0". simpl. apply ev_0.
  Case "E = ev_SS n' E'". simpl. apply E'.  Qed.

(** **** Exercise: 1 star, optional (ev_minus2_n) *)
(** What happens if we try to use [destruct] on [n] instead of [inversion] on [E]? *)

(* FILL IN HERE *)
(** [] *)

(** *** *)
(** Another example, in which [inversion] helps narrow down to
the relevant cases. *)

Theorem SSev__even : forall n,
  ev (S (S n)) -> ev n.
Proof.
  intros n E.
  inversion E as [| n' E'].
  apply E'. Qed.

(** ** [inversion] revisited *)

(** These uses of [inversion] may seem a bit mysterious at first.
    Until now, we've only used [inversion] on equality
    propositions, to utilize injectivity of constructors or to
    discriminate between different constructors.  But we see here
    that [inversion] can also be applied to analyzing evidence
    for inductively defined propositions.

    (You might also expect that [destruct] would be a more suitable
    tactic to use here. Indeed, it is possible to use [destruct], but
    it often throws away useful information, and the [eqn:] qualifier
    doesn't help much in this case.)

    Here's how [inversion] works in general.  Suppose the name
    [I] refers to an assumption [P] in the current context, where
    [P] has been defined by an [Inductive] declaration.  Then,
    for each of the constructors of [P], [inversion I] generates
    a subgoal in which [I] has been replaced by the exact,
    specific conditions under which this constructor could have
    been used to prove [P].  Some of these subgoals will be
    self-contradictory; [inversion] throws these away.  The ones
    that are left represent the cases that must be proved to
    establish the original goal.

    In this particular case, the [inversion] analyzed the construction
    [ev (S (S n))], determined that this could only have been
    constructed using [ev_SS], and generated a new subgoal with the
    arguments of that constructor as new hypotheses.  (It also
    produced an auxiliary equality, which happens to be useless here.)
    We'll begin exploring this more general behavior of inversion in
    what follows. *)

(** **** Exercise: 1 star (inversion_practice) *)
Theorem SSSSev__even : forall n,
  ev (S (S (S (S n)))) -> ev n.
Proof.
  (* FILL IN HERE *) Admitted.

(** The [inversion] tactic can also be used to derive goals by showing
    the absurdity of a hypothesis. *)

Theorem even5_nonsense :
  ev 5 -> 2 + 2 = 9.
Proof.
  (* FILL IN HERE *) Admitted.
(** [] *)

(** **** Exercise: 3 stars, advanced (ev_ev__ev) *)
(** Finding the appropriate thing to do induction on is a
    bit tricky here: *)

Theorem ev_ev__ev : forall n m,
  ev (n+m) -> ev n -> ev m.
Proof.
  (* FILL IN HERE *) Admitted.
(** [] *)

(** **** Exercise: 3 stars, optional (ev_plus_plus) *)
(** Here's an exercise that just requires applying existing lemmas.  No
    induction or even case analysis is needed, but some of the rewriting
    may be tedious. *)

Theorem ev_plus_plus : forall n m p,
  ev (n+m) -> ev (n+p) -> ev (m+p).
Proof.
  (* FILL IN HERE *) Admitted.
(** [] *)

(* ####################################################### *)
(** * Additional Exercises *)

(** **** Exercise: 4 stars (palindromes) *)
(** A palindrome is a sequence that reads the same backwards as
    forwards.

    - Define an inductive proposition [pal] on [list X] that
      captures what it means to be a palindrome. (Hint: You'll need
      three cases.  Your definition should be based on the structure
      of the list; just having a single constructor
    c : forall l, l = rev l -> pal l
      may seem obvious, but will not work very well.)

    - Prove that
       forall l, pal (l ++ rev l).
    - Prove that
       forall l, pal l -> l = rev l.
*)

(* FILL IN HERE *)
(** [] *)

(** **** Exercise: 5 stars, optional (palindrome_converse) *)
(** Using your definition of [pal] from the previous exercise, prove
    that
     forall l, l = rev l -> pal l.
*)

(* FILL IN HERE *)
(** [] *)

(** **** Exercise: 4 stars, advanced (subsequence) *)
(** A list is a _subsequence_ of another list if all of the elements
    in the first list occur in the same order in the second list,
    possibly with some extra elements in between. For example,
    [1,2,3]
    is a subsequence of each of the lists
    [1,2,3]
    [1,1,1,2,2,3]
    [1,2,7,3]
    [5,6,1,9,9,2,7,3,8]
    but it is _not_ a subsequence of any of the lists
    [1,2]
    [1,3]
    [5,6,2,1,7,3,8]

    - Define an inductive proposition [subseq] on [list nat] that
      captures what it means to be a subsequence. (Hint: You'll need
      three cases.)

    - Prove that subsequence is reflexive, that is, any list is a
      subsequence of itself.

    - Prove that for any lists [l1], [l2], and [l3], if [l1] is a
      subsequence of [l2], then [l1] is also a subsequence of [l2 ++
      l3].

    - (Optional, harder) Prove that subsequence is transitive -- that
      is, if [l1] is a subsequence of [l2] and [l2] is a subsequence
      of [l3], then [l1] is a subsequence of [l3].  Hint: choose your
      induction carefully!
*)

(* FILL IN HERE *)
(** [] *)

(** **** Exercise: 2 stars, optional (R_provability) *)
(** Suppose we give Coq the following definition:
    Inductive R : nat -> list nat -> Prop :=
      | c1 : R 0 []
      | c2 : forall n l, R n l -> R (S n) (n :: l)
      | c3 : forall n l, R (S n) l -> R n l.
    Which of the following propositions are provable?

    - [R 2 [1,0]]
    - [R 1 [1,2,1,0]]
    - [R 6 [3,2,1,0]]
*)

(** [] *)

(* ####################################################### *)
(** * Relations *)

(** A proposition parameterized by a number (such as [ev] or
    [beautiful]) can be thought of as a _property_ -- i.e., it defines
    a subset of [nat], namely those numbers for which the proposition
    is provable.  In the same way, a two-argument proposition can be
    thought of as a _relation_ -- i.e., it defines a set of pairs for
    which the proposition is provable. *)

Module LeModule.

(** One useful example is the "less than or equal to"
    relation on numbers. *)

(** The following definition should be fairly intuitive.  It
    says that there are two ways to give evidence that one number is
    less than or equal to another: either observe that they are the
    same number, or give evidence that the first is less than or equal
    to the predecessor of the second. *)

Inductive le : nat -> nat -> Prop :=
  | le_n : forall n, le n n
  | le_S : forall n m, (le n m) -> (le n (S m)).

Notation "m <= n" := (le m n).

(** Proofs of facts about [<=] using the constructors [le_n] and
    [le_S] follow the same patterns as proofs about properties, like
    [ev] in chapter [Prop].  We can [apply] the constructors to prove [<=]
    goals (e.g., to show that [3<=3] or [3<=6]), and we can use
    tactics like [inversion] to extract information from [<=]
    hypotheses in the context (e.g., to prove that [(2 <= 1) -> 2+2=5].) *)

(** *** *)
(** Here are some sanity checks on the definition.  (Notice that,
    although these are the same kind of simple "unit tests" as we gave
    for the testing functions we wrote in the first few lectures, we
    must construct their proofs explicitly -- [simpl] and
    [reflexivity] don't do the job, because the proofs aren't just a
    matter of simplifying computations.) *)

Theorem test_le1 :
  3 <= 3.
Proof.
  (* WORKED IN CLASS *)
  apply le_n.  Qed.

Theorem test_le2 :
  3 <= 6.
Proof.
  (* WORKED IN CLASS *)
  apply le_S. apply le_S. apply le_S. apply le_n.  Qed.

Theorem test_le3 :
  (2 <= 1) -> 2 + 2 = 5.
Proof.
  (* WORKED IN CLASS *)
  intros H. inversion H. inversion H2.  Qed.

(** *** *)
(** The "strictly less than" relation [n < m] can now be defined
    in terms of [le]. *)

End LeModule.

Definition lt (n m:nat) := le (S n) m.

Notation "m < n" := (lt m n).

(** Here are a few more simple relations on numbers: *)

Inductive square_of : nat -> nat -> Prop :=
  sq : forall n:nat, square_of n (n * n).

Inductive next_nat (n:nat) : nat -> Prop :=
  | nn : next_nat n (S n).

Inductive next_even (n:nat) : nat -> Prop :=
  | ne_1 : ev (S n) -> next_even n (S n)
  | ne_2 : ev (S (S n)) -> next_even n (S (S n)).

(** **** Exercise: 2 stars (total_relation) *)
(** Define an inductive binary relation [total_relation] that holds
    between every pair of natural numbers. *)

(* FILL IN HERE *)
(** [] *)

(** **** Exercise: 2 stars (empty_relation) *)
(** Define an inductive binary relation [empty_relation] (on numbers)
    that never holds. *)

(* FILL IN HERE *)
(** [] *)

(** **** Exercise: 2 stars, optional (le_exercises) *)
(** Here are a number of facts about the [<=] and [<] relations that
    we are going to need later in the course.  The proofs make good
    practice exercises. *)

Lemma le_trans : forall m n o, m <= n -> n <= o -> m <= o.
Proof.
  (* FILL IN HERE *) Admitted.

Theorem O_le_n : forall n,
  0 <= n.
Proof.
  (* FILL IN HERE *) Admitted.

Theorem n_le_m__Sn_le_Sm : forall n m,
  n <= m -> S n <= S m.
Proof.
  (* FILL IN HERE *) Admitted.

Theorem Sn_le_Sm__n_le_m : forall n m,
  S n <= S m -> n <= m.
Proof.
  (* FILL IN HERE *) Admitted.

Theorem le_plus_l : forall a b,
  a <= a + b.
Proof.
  (* FILL IN HERE *) Admitted.

Theorem plus_lt : forall n1 n2 m,
  n1 + n2 < m ->
  n1 < m /\ n2 < m.
Proof.
 unfold lt.
 (* FILL IN HERE *) Admitted.

Theorem lt_S : forall n m,
  n < m ->
  n < S m.
Proof.
  (* FILL IN HERE *) Admitted.

Theorem ble_nat_true : forall n m,
  ble_nat n m = true -> n <= m.
Proof.
  (* FILL IN HERE *) Admitted.

Theorem le_ble_nat : forall n m,
  n <= m ->
  ble_nat n m = true.
Proof.
  (* Hint: This may be easiest to prove by induction on [m]. *)
  (* FILL IN HERE *) Admitted.

Theorem ble_nat_true_trans : forall n m o,
  ble_nat n m = true -> ble_nat m o = true -> ble_nat n o = true.
Proof.
  (* Hint: This theorem can be easily proved without using [induction]. *)
  (* FILL IN HERE *) Admitted.

(** **** Exercise: 2 stars, optional (ble_nat_false) *)
Theorem ble_nat_false : forall n m,
  ble_nat n m = false -> ~(n <= m).
Proof.
  (* FILL IN HERE *) Admitted.
(** [] *)

(** **** Exercise: 3 stars (R_provability2) *)
Module R.
(** We can define three-place relations, four-place relations,
    etc., in just the same way as binary relations.  For example,
    consider the following three-place relation on numbers: *)

Inductive R : nat -> nat -> nat -> Prop :=
   | c1 : R 0 0 0
   | c2 : forall m n o, R m n o -> R (S m) n (S o)
   | c3 : forall m n o, R m n o -> R m (S n) (S o)
   | c4 : forall m n o, R (S m) (S n) (S (S o)) -> R m n o
   | c5 : forall m n o, R m n o -> R n m o.

(** - Which of the following propositions are provable?
      - [R 1 1 2]
      - [R 2 2 6]

    - If we dropped constructor [c5] from the definition of [R],
      would the set of provable propositions change?  Briefly (1
      sentence) explain your answer.

    - If we dropped constructor [c4] from the definition of [R],
      would the set of provable propositions change?  Briefly (1
      sentence) explain your answer.

(* FILL IN HERE *)
[]
*)

(** **** Exercise: 3 stars, optional (R_fact) *)
(** Relation [R] actually encodes a familiar function.  State and prove two
    theorems that formally connects the relation and the function.
    That is, if [R m n o] is true, what can we say about [m],
    [n], and [o], and vice versa?
*)

(* FILL IN HERE *)
(** [] *)

End R.

(* ##################################################### *)
(** * Programming with Propositions Revisited *)

(** As we have seen, a _proposition_ is a statement expressing a factual claim,
    like "two plus two equals four."  In Coq, propositions are written
    as expressions of type [Prop]. . *)

Check (2 + 2 = 4).
(* ===> 2 + 2 = 4 : Prop *)

Check (ble_nat 3 2 = false).
(* ===> ble_nat 3 2 = false : Prop *)

Check (beautiful 8).
(* ===> beautiful 8 : Prop *)

(** *** *)
(** Both provable and unprovable claims are perfectly good
    propositions.  Simply _being_ a proposition is one thing; being
    _provable_ is something else! *)

Check (2 + 2 = 5).
(* ===> 2 + 2 = 5 : Prop *)

Check (beautiful 4).
(* ===> beautiful 4 : Prop *)

(** Both [2 + 2 = 4] and [2 + 2 = 5] are legal expressions
    of type [Prop]. *)

(** *** *)
(** We've mainly seen one place that propositions can appear in Coq: in
    [Theorem] (and [Lemma] and [Example]) declarations. *)

Theorem plus_2_2_is_4 :
  2 + 2 = 4.
Proof. reflexivity.  Qed.

(** But they can be used in many other ways.  For example, we have also seen that
    we can give a name to a proposition using a [Definition], just as we have
    given names to expressions of other sorts. *)

Definition plus_fact : Prop  :=  2 + 2 = 4.
Check plus_fact.
(* ===> plus_fact : Prop *)

(** We can later use this name in any situation where a proposition is
    expected -- for example, as the claim in a [Theorem] declaration. *)

Theorem plus_fact_is_true :
  plus_fact.
Proof. reflexivity.  Qed.

(** *** *)
(** We've seen several ways of constructing propositions.

       - We can define a new proposition primitively using [Inductive].

       - Given two expressions [e1] and [e2] of the same type, we can
         form the proposition [e1 = e2], which states that their
         values are equal.

       - We can combine propositions using implication and
         quantification. *)
(** *** *)
(** We have also seen _parameterized propositions_, such as [even] and
    [beautiful]. *)

Check (even 4).
(* ===> even 4 : Prop *)
Check (even 3).
(* ===> even 3 : Prop *)
Check even.
(* ===> even : nat -> Prop *)

(** *** *)
(** The type of [even], i.e., [nat->Prop], can be pronounced in
    three equivalent ways: (1) "[even] is a _function_ from numbers to
    propositions," (2) "[even] is a _family_ of propositions, indexed
    by a number [n]," or (3) "[even] is a _property_ of numbers."  *)

(** Propositions -- including parameterized propositions -- are
    first-class citizens in Coq.  For example, we can define functions
    from numbers to propositions... *)

Definition between (n m o: nat) : Prop :=
  andb (ble_nat n o) (ble_nat o m) = true.

(** ... and then partially apply them: *)

Definition teen : nat->Prop := between 13 19.

(** We can even pass propositions -- including parameterized
    propositions -- as arguments to functions: *)

Definition true_for_zero (P:nat->Prop) : Prop :=
  P 0.

(** *** *)
(** Here are two more examples of passing parameterized propositions
    as arguments to a function.

    The first function, [true_for_all_numbers], takes a proposition
    [P] as argument and builds the proposition that [P] is true for
    all natural numbers. *)

Definition true_for_all_numbers (P:nat->Prop) : Prop :=
  forall n, P n.

(** The second, [preserved_by_S], takes [P] and builds the proposition
    that, if [P] is true for some natural number [n'], then it is also
    true by the successor of [n'] -- i.e. that [P] is _preserved by
    successor_: *)

Definition preserved_by_S (P:nat->Prop) : Prop :=
  forall n', P n' -> P (S n').

(** *** *)
(** Finally, we can put these ingredients together to define
a proposition stating that induction is valid for natural numbers: *)

Definition natural_number_induction_valid : Prop :=
  forall (P:nat->Prop),
    true_for_zero P ->
    preserved_by_S P ->
    true_for_all_numbers P.

(** **** Exercise: 3 stars (combine_odd_even) *)
(** Complete the definition of the [combine_odd_even] function
    below. It takes as arguments two properties of numbers [Podd] and
    [Peven]. As its result, it should return a new property [P] such
    that [P n] is equivalent to [Podd n] when [n] is odd, and
    equivalent to [Peven n] otherwise. *)

Definition combine_odd_even (Podd Peven : nat -> Prop) : nat -> Prop :=
  (* FILL IN HERE *) admit.

(** To test your definition, see whether you can prove the following
    facts: *)

Theorem combine_odd_even_intro :
  forall (Podd Peven : nat -> Prop) (n : nat),
    (oddb n = true -> Podd n) ->
    (oddb n = false -> Peven n) ->
    combine_odd_even Podd Peven n.
Proof.
  (* FILL IN HERE *) Admitted.

Theorem combine_odd_even_elim_odd :
  forall (Podd Peven : nat -> Prop) (n : nat),
    combine_odd_even Podd Peven n ->
    oddb n = true ->
    Podd n.
Proof.
  (* FILL IN HERE *) Admitted.

Theorem combine_odd_even_elim_even :
  forall (Podd Peven : nat -> Prop) (n : nat),
    combine_odd_even Podd Peven n ->
    oddb n = false ->
    Peven n.
Proof.
  (* FILL IN HERE *) Admitted.

(** [] *)

(* ##################################################### *)
(** One more quick digression, for adventurous souls: if we can define
    parameterized propositions using [Definition], then can we also
    define them using [Fixpoint]?  Of course we can!  However, this
    kind of "recursive parameterization" doesn't correspond to
    anything very familiar from everyday mathematics.  The following
    exercise gives a slightly contrived example. *)

(** **** Exercise: 4 stars, optional (true_upto_n__true_everywhere) *)
(** Define a recursive function
    [true_upto_n__true_everywhere] that makes
    [true_upto_n_example] work. *)

(*
Fixpoint true_upto_n__true_everywhere
(* FILL IN HERE *)

Example true_upto_n_example :
    (true_upto_n__true_everywhere 3 (fun n => even n))
  = (even 3 -> even 2 -> even 1 -> forall m : nat, even m).
Proof. reflexivity.  Qed.
*)
(** [] *)

(* $Date: 2014-06-05 07:22:21 -0400 (Thu, 05 Jun 2014) $ *)

author: themattchan

repo: software-foundations


text:
From Hammer Require Import Hammer.

From compcert Require Import Core.
From compcert Require Import Operations.
From compcert Require Import Plus_error.

Section Fprop_mult_error.

Variable beta : radix.
Notation bpow e := (bpow beta e).

Variable prec : Z.
Context { prec_gt_0_ : Prec_gt_0 prec }.

Notation format := (generic_format beta (FLX_exp prec)).
Notation cexp := (cexp beta (FLX_exp prec)).

Variable rnd : R -> Z.
Context { valid_rnd : Valid_rnd rnd }.

Lemma mult_error_FLX_aux:
forall x y,
format x -> format y ->
(round beta (FLX_exp prec) rnd (x * y) - (x * y) <> 0)%R ->
exists f:float beta,
(F2R f = round beta (FLX_exp prec) rnd (x * y) - (x * y))%R
/\ (cexp (F2R f) <= Fexp f)%Z
/\ (Fexp f = cexp x + cexp y)%Z.
Proof with auto with typeclass_instances. hammer_hook "Mult_error" "Mult_error.mult_error_FLX_aux".
intros x y Hx Hy Hz.
set (f := (round beta (FLX_exp prec) rnd (x * y))).
destruct (Req_dec (x * y) 0) as [Hxy0|Hxy0].
contradict Hz.
rewrite Hxy0.
rewrite round_0...
ring.
destruct (mag beta (x * y)) as (exy, Hexy).
specialize (Hexy Hxy0).
destruct (mag beta (f - x * y)) as (er, Her).
specialize (Her Hz).
destruct (mag beta x) as (ex, Hex).
assert (Hx0: (x <> 0)%R).
contradict Hxy0.
now rewrite Hxy0, Rmult_0_l.
specialize (Hex Hx0).
destruct (mag beta y) as (ey, Hey).
assert (Hy0: (y <> 0)%R).
contradict Hxy0.
now rewrite Hxy0, Rmult_0_r.
specialize (Hey Hy0).

assert (Hc1: (cexp (x * y)%R - prec <= cexp x + cexp y)%Z).
unfold cexp, FLX_exp.
rewrite mag_unique with (1 := Hex).
rewrite mag_unique with (1 := Hey).
rewrite mag_unique with (1 := Hexy).
cut (exy - 1 < ex + ey)%Z. omega.
apply (lt_bpow beta).
apply Rle_lt_trans with (1 := proj1 Hexy).
rewrite Rabs_mult.
rewrite bpow_plus.
apply Rmult_le_0_lt_compat.
apply Rabs_pos.
apply Rabs_pos.
apply Hex.
apply Hey.

assert (Hc2: (cexp x + cexp y <= cexp (x * y)%R)%Z).
unfold cexp, FLX_exp.
rewrite mag_unique with (1 := Hex).
rewrite mag_unique with (1 := Hey).
rewrite mag_unique with (1 := Hexy).
cut ((ex - 1) + (ey - 1) < exy)%Z.
generalize (prec_gt_0 prec).
clear ; omega.
apply (lt_bpow beta).
apply Rle_lt_trans with (2 := proj2 Hexy).
rewrite Rabs_mult.
rewrite bpow_plus.
apply Rmult_le_compat.
apply bpow_ge_0.
apply bpow_ge_0.
apply Hex.
apply Hey.

assert (Hr: ((F2R (Float beta (- (Ztrunc (scaled_mantissa beta (FLX_exp prec) x) *
Ztrunc (scaled_mantissa beta (FLX_exp prec) y)) + rnd (scaled_mantissa beta (FLX_exp prec) (x * y)) *
beta ^ (cexp (x * y)%R - (cexp x + cexp y))) (cexp x + cexp y))) = f - x * y)%R).
rewrite Hx at 6.
rewrite Hy at 6.
rewrite <- F2R_mult.
simpl.
unfold f, round, Rminus.
rewrite <- F2R_opp, Rplus_comm, <- F2R_plus.
unfold Fplus. simpl.
now rewrite Zle_imp_le_bool with (1 := Hc2).

exists (Float beta (- (Ztrunc (scaled_mantissa beta (FLX_exp prec) x) *
Ztrunc (scaled_mantissa beta (FLX_exp prec) y)) + rnd (scaled_mantissa beta (FLX_exp prec) (x * y)) *
beta ^ (cexp (x * y)%R - (cexp x + cexp y))) (cexp x + cexp y)).
split;[assumption|split].
rewrite Hr.
simpl.
clear Hr.
apply Z.le_trans with (cexp (x * y)%R - prec)%Z.
unfold cexp, FLX_exp.
apply Zplus_le_compat_r.
rewrite mag_unique with (1 := Hexy).
apply mag_le_bpow with (1 := Hz).
replace (bpow (exy - prec)) with (ulp beta (FLX_exp prec) (x * y)).
apply error_lt_ulp...
rewrite ulp_neq_0; trivial.
unfold cexp.
now rewrite mag_unique with (1 := Hexy).
apply Hc1.
reflexivity.
Qed.

Theorem mult_error_FLX :
forall x y,
format x -> format y ->
format (round beta (FLX_exp prec) rnd (x * y) - (x * y))%R.
Proof. hammer_hook "Mult_error" "Mult_error.mult_error_FLX".
intros x y Hx Hy.
destruct (Req_dec (round beta (FLX_exp prec) rnd (x * y) - x * y) 0) as [Hr0|Hr0].
rewrite Hr0.
apply generic_format_0.
destruct (mult_error_FLX_aux x y Hx Hy Hr0) as ((m,e),(H1,(H2,H3))).
rewrite <- H1.
now apply generic_format_F2R.
Qed.

Lemma mult_bpow_exact_FLX :
forall x e,
format x ->
format (x * bpow e)%R.
Proof. hammer_hook "Mult_error" "Mult_error.mult_bpow_exact_FLX".
intros x e Fx.
destruct (Req_dec x 0) as [Zx|Nzx].
{ rewrite Zx, Rmult_0_l; apply generic_format_0. }
rewrite Fx.
set (mx := Ztrunc _); set (ex := cexp _).
pose (f := {| Fnum := mx; Fexp := ex + e |} : float beta).
apply (generic_format_F2R' _ _ _ f).
{ now unfold F2R; simpl; rewrite bpow_plus, Rmult_assoc. }
intro Nzmx; unfold mx, ex; rewrite <- Fx.
unfold f, ex; simpl; unfold cexp; rewrite (mag_mult_bpow _ _ _ Nzx).
unfold FLX_exp; omega.
Qed.

End Fprop_mult_error.

Section Fprop_mult_error_FLT.

Variable beta : radix.
Notation bpow e := (bpow beta e).

Variable emin prec : Z.
Context { prec_gt_0_ : Prec_gt_0 prec }.

Notation format := (generic_format beta (FLT_exp emin prec)).
Notation cexp := (cexp beta (FLT_exp emin prec)).

Variable rnd : R -> Z.
Context { valid_rnd : Valid_rnd rnd }.

Theorem mult_error_FLT :
forall x y,
format x -> format y ->
(x * y <> 0 -> bpow (emin + 2*prec - 1) <= Rabs (x * y))%R ->
format (round beta (FLT_exp emin prec) rnd (x * y) - (x * y))%R.
Proof with auto with typeclass_instances. hammer_hook "Mult_error" "Mult_error.mult_error_FLT".
intros x y Hx Hy Hxy.
set (f := (round beta (FLT_exp emin prec) rnd (x * y))).
destruct (Req_dec (f - x * y) 0) as [Hr0|Hr0].
rewrite Hr0.
apply generic_format_0.
destruct (Req_dec (x * y) 0) as [Hxy'|Hxy'].
unfold f.
rewrite Hxy'.
rewrite round_0...
ring_simplify (0 - 0)%R.
apply generic_format_0.
specialize (Hxy Hxy').
destruct (mult_error_FLX_aux beta prec rnd x y) as ((m,e),(H1,(H2,H3))).
now apply generic_format_FLX_FLT with emin.
now apply generic_format_FLX_FLT with emin.
rewrite <- (round_FLT_FLX beta emin).
assumption.
apply Rle_trans with (2:=Hxy).
apply bpow_le.
generalize (prec_gt_0 prec).
clear ; omega.
rewrite <- (round_FLT_FLX beta emin) in H1.
2:apply Rle_trans with (2:=Hxy).
2:apply bpow_le ; generalize (prec_gt_0 prec) ; clear ; omega.
unfold f; rewrite <- H1.
apply generic_format_F2R.
intros _.
simpl in H2, H3.
unfold cexp, FLT_exp.
case (Zmax_spec (mag beta (F2R (Float beta m e)) - prec) emin);
intros (M1,M2); rewrite M2.
apply Z.le_trans with (2:=H2).
unfold cexp, FLX_exp.
apply Z.le_refl.
rewrite H3.
unfold cexp, FLX_exp.
assert (Hxy0:(x*y <> 0)%R).
contradict Hr0.
unfold f.
rewrite Hr0.
rewrite round_0...
ring.
assert (Hx0: (x <> 0)%R).
contradict Hxy0.
now rewrite Hxy0, Rmult_0_l.
assert (Hy0: (y <> 0)%R).
contradict Hxy0.
now rewrite Hxy0, Rmult_0_r.
destruct (mag beta x) as (ex,Ex) ; simpl.
specialize (Ex Hx0).
destruct (mag beta y) as (ey,Ey) ; simpl.
specialize (Ey Hy0).
assert (emin + 2 * prec -1 < ex + ey)%Z.
2: omega.
apply (lt_bpow beta).
apply Rle_lt_trans with (1:=Hxy).
rewrite Rabs_mult, bpow_plus.
apply Rmult_le_0_lt_compat; try apply Rabs_pos.
apply Ex.
apply Ey.
Qed.

Lemma F2R_ge: forall (y:float beta),
(F2R y <> 0)%R -> (bpow (Fexp y) <= Rabs (F2R y))%R.
Proof. hammer_hook "Mult_error" "Mult_error.F2R_ge".
intros (ny,ey).
rewrite <- F2R_Zabs; unfold F2R; simpl.
case (Zle_lt_or_eq 0 (Z.abs ny)).
apply Z.abs_nonneg.
intros Hy _.
rewrite <- (Rmult_1_l (bpow _)) at 1.
apply Rmult_le_compat_r.
apply bpow_ge_0.
apply IZR_le; omega.
intros H1 H2; contradict H2.
replace ny with 0%Z.
simpl; ring.
now apply sym_eq, Z.abs_0_iff, sym_eq.
Qed.

Theorem mult_error_FLT_ge_bpow :
forall x y e,
format x -> format y ->
(bpow (e+2*prec-1) <= Rabs (x * y))%R ->
(round beta (FLT_exp emin prec) rnd (x * y) - (x * y) <> 0)%R ->
(bpow e <= Rabs (round beta (FLT_exp emin prec) rnd (x * y) - (x * y)))%R.
Proof with auto with typeclass_instances. hammer_hook "Mult_error" "Mult_error.mult_error_FLT_ge_bpow".
intros x y e.
set (f := (round beta (FLT_exp emin prec) rnd (x * y))).
intros Fx Fy H1.
unfold f; rewrite Fx, Fy, <- F2R_mult.
simpl Fmult.
destruct (round_repr_same_exp beta (FLT_exp emin prec)
rnd (Ztrunc (scaled_mantissa beta (FLT_exp emin prec) x) *
Ztrunc (scaled_mantissa beta (FLT_exp emin prec) y))
(cexp x + cexp y)) as (n,Hn).
rewrite Hn; clear Hn.
rewrite <- F2R_minus, Fminus_same_exp.
intros K.
eapply Rle_trans with (2:=F2R_ge _ K).
simpl (Fexp _).
apply bpow_le.
unfold cexp, FLT_exp.
destruct (mag beta x) as (ex,Hx).
destruct (mag beta y) as (ey,Hy).
simpl; apply Z.le_trans with ((ex-prec)+(ey-prec))%Z.
2: apply Zplus_le_compat; apply Z.le_max_l.
assert (e + 2*prec -1< ex+ey)%Z;[idtac|omega].
apply lt_bpow with beta.
apply Rle_lt_trans with (1:=H1).
rewrite Rabs_mult, bpow_plus.
apply Rmult_lt_compat.
apply Rabs_pos.
apply Rabs_pos.
apply Hx.
intros K'; contradict H1; apply Rlt_not_le.
rewrite K', Rmult_0_l, Rabs_R0; apply bpow_gt_0.
apply Hy.
intros K'; contradict H1; apply Rlt_not_le.
rewrite K', Rmult_0_r, Rabs_R0; apply bpow_gt_0.
Qed.

Lemma mult_bpow_exact_FLT :
forall x e,
format x ->
(emin + prec - mag beta x <= e)%Z ->
format (x * bpow e)%R.
Proof. hammer_hook "Mult_error" "Mult_error.mult_bpow_exact_FLT".
intros x e Fx He.
destruct (Req_dec x 0) as [Zx|Nzx].
{ rewrite Zx, Rmult_0_l; apply generic_format_0. }
rewrite Fx.
set (mx := Ztrunc _); set (ex := cexp _).
pose (f := {| Fnum := mx; Fexp := ex + e |} : float beta).
apply (generic_format_F2R' _ _ _ f).
{ now unfold F2R; simpl; rewrite bpow_plus, Rmult_assoc. }
intro Nzmx; unfold mx, ex; rewrite <- Fx.
unfold f, ex; simpl; unfold cexp; rewrite (mag_mult_bpow _ _ _ Nzx).
unfold FLT_exp; rewrite Z.max_l; [|omega]; rewrite <- Z.add_max_distr_r.
set (n := (_ - _ + _)%Z); apply (Z.le_trans _ n); [unfold n; omega|].
apply Z.le_max_l.
Qed.

End Fprop_mult_error_FLT.

author: lukaszcz

repo: coqhammer-eval