Hoare論理っぽいもの

hoare.v

Require Import Arith.
(*
Check eq_nat_dec.

Definition update {A B : Set} (eq_dec : forall x y : A, {x = y} + {x <> y}) (f : A -> B) (x : A) (a : B) : A -> B :=
fun y => match eq_dec x y with
| left _ => a
| right _ => f y
end.
Check nat.
Eval compute in (update eq_nat_dec (fun x => S x) 1 1 2).
*)

Definition update {A : Set} (f : nat -> A) (x : nat) (a : A) :=
fun y => if beq_nat x y then a else f y.

Lemma update_eq_lemma : forall (A : Set) (f : nat -> A) (x : nat) (a : A), update f x a x = a.
intros.
unfold update.
rewrite <- beq_nat_refl.
reflexivity.
Qed.

Lemma update_neq_lemma : forall (A : Set) (f : nat -> A) (x y : nat) (a : A), x<>y -> update f x a y = f y.
intros.
unfold update.
case_eq (beq_nat x y).
intro.
contradict H.
apply beq_nat_eq.
symmetry.
assumption.
trivial.
Qed.

Inductive Val {A : Set} : Set :=
| Var : nat -> Val
| Const : A -> Val.

Definition evalV {A : Set} (env : nat -> A) (v : Val) : A :=
match v with
| Var i => env i
| Const a => a
end.

Definition env_type := ((nat -> nat) * (nat -> bool))%type.

Inductive ArithExp : Set :=
| ValA : Val (A:=nat) -> ArithExp
| AddA : ArithExp -> ArithExp -> ArithExp.

Fixpoint evalAE (env : env_type) (e : ArithExp) : nat :=
let (envA, envB) := env in
match e with
| ValA v => evalV envA v
| AddA e1 e2 => evalAE env e1 + evalAE env e2
end.

Inductive BoolExp : Set :=
| ValB : Val (A:=bool) -> BoolExp
| AndB : BoolExp -> BoolExp -> BoolExp
| OrB : BoolExp -> BoolExp -> BoolExp
| NotB : BoolExp -> BoolExp
| LeB : ArithExp -> ArithExp -> BoolExp.

Print "&&".

Fixpoint evalBE (env : env_type) (e : BoolExp) : bool :=
let (envA, envB) := env in
match e with
| ValB v => evalV envB v
| AndB e1 e2 => ((evalBE env e1) && (evalBE env e2))%bool
| OrB e1 e2 => (evalBE env e1 || evalBE env e2)%bool
| NotB e => negb (evalBE env e)
| LeB a1 a2 => leb (evalAE env a1) (evalAE env a2)
end.

Inductive Cmd : Set :=
| SkipC : Cmd
| AssignArithC : nat -> ArithExp -> Cmd
| ConsC : Cmd -> Cmd -> Cmd
| IfC : BoolExp -> Cmd -> Cmd -> Cmd
| WhileC : BoolExp -> Cmd -> Cmd.

Fixpoint evalC (n : nat) (env : env_type) (c : Cmd) : option env_type :=
let (envA, envB) := env in
match n with
| 0 => None
| S n' =>
  match c with
  | SkipC => Some env
  | AssignArithC x ae => Some (update envA x (evalAE env ae), envB)
  | ConsC c1 c2 =>
    match evalC n' env c1 with
    | None => None
    | Some env' => evalC n' env' c2
    end
  | IfC be ct cf => if evalBE env be then evalC n' env ct else evalC n' env cf
  | WhileC be c' => evalC n' env (IfC be (ConsC c' c) SkipC)
  end
end.

Lemma evalC_lemma1 : forall (m n : nat) (c : Cmd) (env env' : env_type), m <= n -> Some env' = evalC m env c -> Some env' = evalC n env c.
induction m.
simpl.
destruct env.
congruence.
intros.
assert (n = S (pred n)).
apply (S_pred n m);assumption.
rewrite H1.
revert H0.
rewrite H1 in H.
apply le_S_n in H.
clear H1.
destruct env as [envA envB].
destruct env' as [envA' envB'].
case c;simpl.
trivial.
trivial.
intros c1 c2.
case_eq (evalC m (envA, envB) c1);[|congruence].
destruct e as [envA'' envB''].
intros.
rewrite <- (IHm (pred n) c1 (envA, envB) (envA'', envB'')).
apply (IHm (pred n) c2 (envA'', envB'') (envA', envB'));assumption.
assumption.
symmetry.
assumption.

intros b ct cf.
case (evalBE (envA, envB) b).
apply (IHm (pred n) ct (envA, envB) (envA', envB'));assumption.
apply (IHm (pred n) cf (envA, envB) (envA', envB'));assumption.

intros.
apply (IHm (pred n) (IfC b (ConsC c0 (WhileC b c0)) SkipC) (envA, envB) (envA', envB'));assumption.
Qed.

Goal forall (envA : nat -> nat) (envB : nat -> bool) (x : nat) (ae : ArithExp) (n : nat), exists (envA' : nat->nat), Some (envA', envB) = evalC (S n) (envA, envB) (AssignArithC x ae) /\ envA' x = evalAE (envA, envB) ae.
(* = Some (evalAE envA ae, envB).*)
Proof.
  intros.
  simpl.
  exists (update envA x (evalAE (envA, envB) ae)).
  split;[reflexivity|].
  apply update_eq_lemma.
Qed.

Definition hoare_triple_type := ((env_type -> Prop) * Cmd * (env_type -> Prop))%type.

Definition partially_correct (h : hoare_triple_type) : Prop :=
let (pre_c, post) := h in let (pre, c) := pre_c in forall (env env' : env_type) (n : nat), pre env -> Some env' = evalC n env c -> post env'.

Lemma composition_lemma : forall (p q r : env_type -> Prop) (c1 c2 : Cmd), partially_correct (p, c1, q) -> partially_correct (q, c2, r) -> partially_correct (p, ConsC c1 c2, r).
Proof.
  unfold partially_correct.
  intros.
  destruct n.
  contradict H2.
  simpl.
  destruct env.
  congruence.
  simpl in H2.
  destruct env as [envA envB].
  revert H2.
  case_eq (evalC n (envA, envB) c1).
  intros.
  apply (H0 e env' n).
  apply (H (envA, envB) e n).
  assumption.
  auto.
  assumption.
  discriminate.
Qed.

Goal forall n : nat, partially_correct (fun env : env_type => (let (envA, _) := env in envA 0) = n, AssignArithC 0 (AddA (ValA (Var 0)) (ValA (Const 1))), fun env : env_type => (let (envA, _) := env in envA 0) = S n).
Proof.
  unfold partially_correct.
  intros.
  destruct env' as [envA' envB'].
  destruct env as [envA envB].
  revert H0.
  destruct n0;simpl.
  congruence.
  rewrite H.
  intro.
  injection H0.
  intros.
  rewrite H2.
  rewrite update_eq_lemma.
  rewrite plus_comm.
  auto.
Qed.

Lemma conditional_lemma : forall (be : BoolExp) (ct cf : Cmd) (p q : env_type -> Prop),
 partially_correct (fun env : env_type => evalBE env be = true /\ p env, ct, q) ->
 partially_correct (fun env : env_type => evalBE env be = false /\ p env, cf, q) ->
 partially_correct (p, IfC be ct cf, q).
unfold partially_correct.
intros.
revert H2.
destruct n;simpl;destruct env as [envA envB].
congruence.
case_eq (evalBE (envA, envB) be);intros.
apply (H (envA, envB) env' n).
split;assumption.
assumption.
apply (H0 (envA, envB) env' n).
split;assumption.
assumption.
Qed.

Lemma while_lemma : forall (be : BoolExp) (c : Cmd) (p : env_type -> Prop),
 partially_correct (fun env : env_type => evalBE env be = true /\ p env, c, p) ->
 partially_correct (p, WhileC be c, fun env : env_type => evalBE env be = false /\ p env).
unfold partially_correct.
intros be c p H env env' n.
destruct env as [envA envB].
destruct env' as [envA' envB'].
revert be c p H envA envB envA' envB'.
induction n;simpl;intros.
congruence.
revert H1.
destruct n;simpl;[congruence|].
case_eq (evalBE (envA, envB) be).
intro.
destruct n;simpl;[congruence|].
case_eq (evalC n (envA, envB) c).
intros.
destruct e as [envA'' envB''].
apply IHn with c envA'' envB''.
assumption.
Focus 3.
congruence.
Focus 3.
intro.
destruct n;simpl;[congruence|].
intro.
injection H2.
intros.
rewrite H3.
rewrite H4.
split;assumption.
Focus 2.
apply evalC_lemma1 with n.
auto.
assumption.
apply (H (envA, envB) (envA'', envB'') n).
split;assumption.
auto.
Qed.

Lemma empty_statement_lemma : forall (p : env_type -> Prop), partially_correct (p, SkipC, p).
unfold partially_correct.
intros.
destruct env.
destruct n;simpl in H0.
congruence.
injection H0.
intro.
rewrite H1.
assumption.
Qed.

Lemma assignment_lemma : forall (p q : env_type -> Prop) (x : nat) (a : ArithExp),
(forall (envA : nat -> nat) (envB : nat -> bool), p (envA, envB) -> q ((update envA x (evalAE (envA, envB) a)), envB)) -> partially_correct (p, AssignArithC x a, q).
unfold partially_correct.
intros.
revert H1.
destruct env as [envA envB].
destruct env' as [envA' envB'].
destruct n;simpl.
congruence.
intro.
injection H1.
intros.
rewrite H2.
rewrite H3.
apply H.
assumption.
Qed.

Goal partially_correct (fun _ => True, ConsC (AssignArithC 0 (ValA (Const 0))) (AssignArithC 1 (ValA (Const 1))), fun env : env_type => let (envA, _) := env in envA 0 = 0 /\ envA 1 = 1).
apply composition_lemma with (fun env : env_type => let (envA, _) := env in envA 0 = 0).
apply assignment_lemma.
intros.
apply update_eq_lemma.
apply assignment_lemma.
intros.
split.
rewrite update_neq_lemma.
assumption.
congruence.
apply update_eq_lemma.
Qed.

Definition terminate (p : env_type -> Prop) (c : Cmd) : Prop := forall env : env_type, p env -> exists (n : nat) (env' : env_type), evalC n env c = Some env'.

Lemma empty_statement_term : forall (p : env_type -> Prop), terminate p SkipC.
intro.
exists 1.
exists env.
simpl.
destruct env.
reflexivity.
Qed.

Check well_founded.
(*See Coq.Arith.Wf_nat*)
Check lt_wf.
(*
Goal well_founded lt.
unfold well_founded.
cut (forall (n m : nat), m <= n -> Acc lt m).
intros H m.
apply (H m).
SearchPattern(_ <= _).
apply le_n.
induction n.
SearchPattern (_ <= 0 -> 0 = _).
intros.
replace m with 0.
apply Acc_intro.
SearchPattern (~_ < 0).
intros.
contradict H0.
apply lt_n_0.
apply le_n_0_eq.
assumption.
intros.
apply le_lt_or_eq_iff in H.
destruct H.
apply le_S_n in H.
apply IHn.
assumption.
rewrite H.
apply Acc_intro.
intros.
apply le_S_n in H0.
apply IHn.
assumption.
Qed.
*)

Lemma consequence_lemma_1 : forall (p p' q : env_type -> Prop) (c : Cmd), (forall env : env_type, p env -> p' env) -> partially_correct (p', c, q) -> partially_correct (p, c, q).
unfold partially_correct.
intros.
apply (H0 env env' n).
apply H.
assumption.
assumption.
Qed.

Lemma consequence_lemma_2 : forall (p q q' : env_type -> Prop) (c : Cmd), (forall env : env_type, q' env -> q env) -> partially_correct (p, c, q') -> partially_correct (p, c, q).
unfold partially_correct.
intros.
apply H.
apply (H0 env env' n);assumption.
Qed.

Definition totally_correct (h : hoare_triple_type) : Prop :=
partially_correct h /\ let (pre_c, post) := h in let (pre, c) := pre_c in terminate pre c.

Lemma while_term : forall (A : Type) (R : A -> A -> Prop) (b : BoolExp) (t : env_type -> A) (c : Cmd) (p : env_type -> Prop), well_founded R ->
 (forall (z : A), totally_correct (fun env => t env = z /\ p env /\ evalBE env b = true, c, fun env => R (t env) z /\ p env)) ->
 terminate p (WhileC b c).
intros.
Check well_founded_ind.
intro.
cut (forall (a : A) (e : env_type), a = t e -> p e -> exists (n : nat) (env' : env_type), evalC n e (WhileC b c) = Some env').
intros.
apply (H1 (t env)).
reflexivity.
assumption.
apply (well_founded_ind H (fun a => forall (e : env_type),
a = t e -> p e ->
exists (n : nat) (env' : env_type), evalC n e (WhileC b c) = Some env')).
assert (forall (e env' : env_type) (n : nat), p e /\ evalBE e b = true /\ evalC n e c = Some env' -> R (t env') (t e) /\ p env').
intros.
destruct (H0 (t e)).
destruct H1.
destruct H4.
apply (H2 e env' n).
split.
reflexivity.
split;assumption.
symmetry.
assumption.
intros.
case_eq (evalBE e b).
Focus 2.
intro.
exists 3.
exists e.
simpl.
destruct e.
rewrite H5.
reflexivity.
intro.

(*apply H2 with x.*)
destruct (H0 (t e)).
clear H6.
specialize (H7 e).
assert (exists (n : nat) (env' : env_type), evalC n e c = Some env').
apply H7.
split;tauto.
clear H7.
destruct H6 as [x0 H6].
destruct H6 as [env' H6].
specialize (H1 e env' x0).
destruct H1.
split;[assumption|split;assumption].

specialize (H2 (t env')).
rewrite H3 in H2.
specialize (H2 H1 env' eq_refl).
destruct H2.
assumption.
destruct H2.

exists (S (S (S (max x0 x1)))).
simpl.
destruct e as [eA eB].
case (evalBE (eA, eB) b).
Focus 2.
exists (eA, eB).
reflexivity.
replace (evalC (max x0 _) (eA, eB) c) with (Some env').
Focus 2.
Check evalC_lemma1.
eapply evalC_lemma1.
SearchPattern (_ <= max _ _).
apply Max.le_max_l.
symmetry.
assumption.
exists x2.
symmetry.
apply evalC_lemma1 with x1.
apply Max.le_max_r.
symmetry.
assumption.
Qed.

Lemma conditional_term : forall (b : BoolExp) (ct cf : Cmd) (p : env_type -> Prop), terminate (fun env => evalBE env b = true /\ p env) ct -> terminate (fun env => evalBE env b = false /\ p env) cf -> terminate p (IfC b ct cf).
unfold terminate.
intros.
specialize (H env).
specialize (H0 env).
case_eq (evalBE env b);intro;destruct env as [envA envB].
destruct H.
split;assumption.
exists (S x).
simpl.
rewrite H2.
assumption.

destruct H0.
split;assumption.
exists (S x).
simpl.
rewrite H2.
assumption.
Qed.

Lemma assignment_term : forall (a : ArithExp) (x : nat) (p : env_type -> Prop), terminate p (AssignArithC x a).
unfold terminate.
intros.
exists 1.
destruct env as [envA envB].
exists (update envA x (evalAE (envA, envB) a), envB).
reflexivity.
Qed.

Lemma composition_term : forall (c1 c2 : Cmd) (p q : env_type -> Prop), totally_correct (p, c1, q) -> terminate q c2 -> terminate p (ConsC c1 c2).
unfold totally_correct.
unfold terminate.
intros c1 c2 p q H H0 env pre_cond.
destruct H as [part_c1 H].
specialize (H env pre_cond).
destruct H as [x1 H1].
destruct H1 as [env' H1].
specialize (part_c1 env env' x1 pre_cond).
assert (pre_cond_q : q env').
apply part_c1.
symmetry.
assumption.
specialize (H0 env' pre_cond_q).
destruct H0 as [x2 H2].
destruct H2 as [env'' H2].
exists (S (max x1 x2)).
exists env''.
simpl.
destruct env as [envA envB].
replace (evalC (max x1 x2) (envA, envB) c1) with (Some env').
symmetry.
Check evalC_lemma1.
apply evalC_lemma1 with x2.
apply Max.le_max_r.
symmetry.
assumption.
apply evalC_lemma1 with x1.
apply Max.le_max_l.
symmetry.
assumption.
Qed.

Lemma empty_statement_total : forall (p : env_type -> Prop), totally_correct (p, SkipC, p).
intro.
split.
apply empty_statement_lemma.
apply empty_statement_term.
Qed.

Goal forall (p q : env_type -> Prop) (x : nat) (a : ArithExp),
(forall (envA : nat -> nat) (envB : nat -> bool), p (envA, envB) -> q ((update envA x (evalAE (envA, envB) a)), envB)) -> totally_correct (p, AssignArithC x a, q).
intros.
split.
apply assignment_lemma.
assumption.
apply assignment_term.
Qed.

Lemma consequence_total_1 : forall (p p' q : env_type -> Prop) (c : Cmd), (forall env : env_type, p env -> p' env) -> totally_correct (p', c, q) -> totally_correct (p, c, q).
intros.
destruct H0.
split.
apply consequence_lemma_1 with p';assumption.
intros env H2.
apply H1.
apply H.
assumption.
Qed.

Lemma consequence_total_2 : forall (p q q' : env_type -> Prop) (c : Cmd), (forall env : env_type, q' env -> q env) -> totally_correct (p, c, q') -> totally_correct (p, c, q).
intros.
destruct H0.
split.
apply consequence_lemma_2 with q';assumption.
assumption.
Qed.

Lemma conditional_total : forall (be : BoolExp) (ct cf : Cmd) (p q : env_type -> Prop),
 totally_correct (fun env : env_type => evalBE env be = true /\ p env, ct, q) ->
 totally_correct (fun env : env_type => evalBE env be = false /\ p env, cf, q) ->
 totally_correct (p, IfC be ct cf, q).
intros.
destruct H.
destruct H0.
split.
apply conditional_lemma;assumption.
apply conditional_term;assumption.
Qed.

Lemma composition_total : forall (p q r : env_type -> Prop) (c1 c2 : Cmd), totally_correct (p, c1, q) -> totally_correct (q, c2, r) -> totally_correct (p, ConsC c1 c2, r).
intros.
destruct H0.
split.
apply composition_lemma with q.
destruct H.
assumption.
assumption.
apply composition_term with q;assumption.
Qed.

Lemma while_total : forall (A : Type) (R : A -> A -> Prop) (b : BoolExp) (t : env_type -> A) (c : Cmd) (p : env_type -> Prop),
 well_founded R ->
 (forall (z : A), totally_correct (fun env => t env = z /\ p env /\ evalBE env b = true, c, fun env => R (t env) z /\ p env)) ->
 totally_correct (p, WhileC b c, fun env => evalBE env b = false /\ p env).
intros.
split.
apply while_lemma.
unfold partially_correct.
intros.
specialize (H0 (t env)).
destruct H0.
specialize (H0 env env' n).
simpl in H0.
destruct H0.
split.
reflexivity.
tauto.
assumption.
assumption.
apply (while_term A R b t c p H).
intro.
specialize (H0 z).
apply consequence_total_2 with (fun env : env_type => R (t env) z /\ p env).
tauto.
assumption.
Qed.

Lemma assignment_total : forall (p q : env_type -> Prop) (x : nat) (a : ArithExp),
(forall (envA : nat -> nat) (envB : nat -> bool), p (envA, envB) -> q ((update envA x (evalAE (envA, envB) a)), envB)) -> totally_correct (p, AssignArithC x a, q).
intros.
split.
apply assignment_lemma.
assumption.
apply assignment_term.
Qed.