(* Structural Operational Semantics (SOS), or smal-steps semantics  *)


Require Import Bool Arith List.
Import List.ListNotations.

(* ========================================================================== *)
(** * Preliminary material *)
(** ** Syntax of arithmetic expressions *)

Inductive aexp :=
| Aco : nat -> aexp
| Ava : nat -> aexp
| Apl : aexp -> aexp -> aexp
| Amu : aexp -> aexp -> aexp
| Asu : aexp -> aexp -> aexp
.

(** ** Syntax of Boolean expressions *)

Inductive bexp :=
| Btrue : bexp
| Bfalse : bexp
| Bnot : bexp -> bexp
| Band : bexp -> bexp -> bexp
| Bor : bexp -> bexp -> bexp
| Beq : bexp -> bexp -> bexp
| Beqnat : aexp -> aexp -> bexp
.

(** ** Syntax of the WHILE language *)

Inductive winstr :=
| Skip   : winstr
| Assign : nat -> aexp -> winstr
| Seq    : winstr -> winstr -> winstr
| If     : bexp -> winstr -> winstr -> winstr
| While  : bexp -> winstr -> winstr
.

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

Definition state := list nat.


Fixpoint get (i:nat) (s:state) : nat :=
  match i,s with
  | 0   ,  v :: _   => v
  | S i',  _ :: s'  => get i' s'
  | _   ,  _        => 0
  end.

Fixpoint update (s:state) (i:nat) (v:nat) : state :=
  match i,s with
  | 0   , a :: s' => v :: s'
  | 0   , []      => v :: nil
  | S i', a :: s' => a :: (update s' i' v)
  | S i', []      => 0 :: (update [] i' v)
  end.

(* ----------------------------------------------- *)
(** Functional semantics of [aexp] and of [bexp]   *)

Fixpoint evalA (a: aexp) (s: state) : nat :=
  match a with
  | Aco n => n
  | Ava x => get x s
  | Apl a1 a2 =>  evalA a1 s + evalA a2 s
  | Amu a1 a2 =>  evalA a1 s * evalA a2 s
  | Asu a1 a2 =>  evalA a1 s - evalA a2 s
  end.

Definition eqboolb b1 b2 : bool :=
  match b1, b2  with
  | true , true  => true
  | false, false => true
  | _    , _     => false
  end.

Fixpoint eqnatb n1 n2 : bool :=
  match n1, n2 with
  | O    , O     => true
  | S n1', S n2' => eqnatb n1' n2'
  | _    , _     => false
  end.

Fixpoint evalB (b : bexp) (s : state) : bool :=
  match b with
  | Btrue => true
  | Bfalse => false
  | Bnot b => negb (evalB b s)
  | Band e1 e2 => (evalB e1 s) && (evalB e2 s)
  | Bor e1 e2 => (evalB e1 s) || (evalB e2 s)
  | Beq e1 e2 => eqboolb (evalB e1 s) (evalB e2 s)
  | Beqnat n1 n2 => eqnatb (evalA n1 s) (evalA n2 s)
  end.


(* ========================================================================== *)

(** * SOS (small steps semantics) of the WHILE language *)

Inductive config :=
| Inter : winstr -> state -> config
| Final : state -> config.

(* The relation for one SOS step *)

Inductive SOS_1: winstr -> state -> config -> Prop :=
| SOS1_Skip     : forall s,
                 SOS_1 Skip s (Final s)

| SOS1_Assign   : forall x a s,
                 SOS_1 (Assign x a) s (Final (update s x (evalA a s)))

| SOS1_Seqf     : forall i1 i2 s s1,
                 SOS_1 i1 s (Final s1) ->
                 SOS_1 (Seq i1 i2) s (Inter i2 s1)
| SOS1_Seqi     : forall i1 i1' i2 s s1,
                 SOS_1 i1 s (Inter i1' s1) ->
                 SOS_1 (Seq i1 i2) s (Inter (Seq i1' i2) s1)

| SOS1_If_true  : forall b i1 i2 s,
                 evalB b s = true  ->
                 SOS_1 (If b i1 i2) s (Inter i1 s)
| SOS1_If_false : forall b i1 i2 s,
                 evalB b s = false ->
                 SOS_1 (If b i1 i2) s (Inter i2 s)

| SOS1_While    : forall b i s,
                 SOS_1 (While b i) s (Inter (If b (Seq i (While b i)) Skip) s)
.

(** Reflexive-transitive closure of [SOS_1] *)
(** This semantics gives all reachable configurations
    for an (AST of) WHILE program, starting with an initial state.
 *)

Inductive SOS : config -> config -> Prop :=
| SOS_stop  : forall c, SOS c c
| SOS_again : forall i1 s1 c2 c3,
              SOS_1 i1 s1 c2 -> SOS c2 c3 ->
              SOS (Inter i1 s1) c3.


(* ========================================================================== *)

Definition N0 := Aco 0.
Definition N1 := Aco 1.
Definition N2 := Aco 2.
Definition N3 := Aco 3.
Definition N4 := Aco 4.


(** * I *)

(** *** Computation of the square of [n] using additions *)
(** Here is a While program Psquare corresponding to à
    while not (i=n) do {i:= 1+i; x:= y+x ; y:= 2+y} *)
Definition Il := 0.
Definition Ir := Ava Il.
Definition Xl := 1.
Definition Xr := Ava Xl.
Definition Yl := 2.
Definition Yr := Ava Yl.

Definition incrI := Assign Il (Apl N1 Ir).
Definition incrX := Assign Xl (Apl Yr Xr).
Definition incrY := Assign Yl (Apl N2 Yr).
Definition body_square := Seq incrI (Seq incrX incrY).
Definition Psquare_2 := While (Bnot (Beqnat Ir (Aco 2))) body_square.
Definition Psquare n := While (Bnot (Beqnat Ir (Aco n))) body_square.
(** New! We can play with looping programs *)
Definition Psquare_inf := While Btrue body_square.

Lemma SOS_Psquare_2_1st_round : SOS (Inter Psquare_2 [0;0;1]) (Inter Psquare_2 [1; 1; 3]).
Proof.
  eapply SOS_again.
  { apply SOS1_While. }
  eapply SOS_again.
  { Compute (evalB (Bnot (Beqnat Ir (Aco 2))) [0; 0; 1]).
    apply SOS1_If_true. reflexivity. }
  eapply SOS_again.
  { apply SOS1_Seqi. apply SOS1_Seqf. apply SOS1_Assign. }
Admitted.

Theorem SOS_Psquare_inf_1st_round : SOS (Inter Psquare_inf [0;0;1]) (Inter Psquare_inf [1; 1; 3]).
Proof.
Admitted.

Theorem SOS_Psquare_2_V0 : SOS (Inter Psquare_2 [0;0;1]) (Final [2;4;5]).
Proof.
Admitted.

(** We want to avoid repetitions, and eventually consider
    the general case Psquare. *)

(** Essential property of [SOS], of practical interest. *)
Theorem SOS_trans : forall c1 c2 c3, SOS c1 c2 -> SOS c2 c3 -> SOS c1 c3.
Proof.
Admitted.

(** You can admit the following one, or just copy-paste the script
    of a previous lemma (nothing new to lear here, but the result
    is needed below). *)
Lemma SOS_Psquare_2_2e_round : SOS (Inter Psquare_2 [1; 1; 3]) (Inter Psquare_2 [2; 4; 5]).
Proof.
Admitted.

Theorem SOS_Psquare_2_end : SOS (Inter Psquare_2 [2; 4; 5]) (Final [2; 4; 5]).
Proof.
Admitted.

(** Smae statement as [SOS_Psquare_2_V0]. Use [SOS_trans] *)
Theorem SOS_Psquare_2_end_V1 : SOS (Inter Psquare_2 [0;0;1]) (Final [2;4;5]).
Proof.
  apply SOS_trans with (Inter Psquare_2 [1; 1; 3]).
Admitted.

(** Generalisation to [Psquare] *)

(** We need two arithmetic lemmas, provable with the [ring] tactic. *)
Lemma Sn_2 n : S n + S n = S (S (n + n)).
Proof. ring. Qed.

Lemma Sn_square n : S n * S n = S (n + n + n * n).
Proof. ring. Qed.

Definition invar_cc n := [n; n*n; S (n+n)].
Theorem SOS_body_square n : SOS (Inter body_square (invar_cc n)) (Final (invar_cc (S n))).
Proof.
Admitted.

(** Short but difficult script. You can admit it or take it 
    as a challenge to be solved later. *)
Fixpoint SOS_seqf i1 i2 s1 s2 (so : SOS (Inter i1 s1) (Final s2)) :
  SOS (Inter (Seq i1 i2) s1) (Inter i2 s2).
Proof.
Admitted.

(** Reuse the previous lemmas (easy and very short). *)
Lemma SOS_body_square_inter n i :
  SOS (Inter (Seq body_square i) (invar_cc n)) (Inter i (invar_cc (S n))).
Proof.
  apply SOS_seqf.
Admitted.

Lemma eqnatb_refl : forall n, eqnatb n n = true.
Proof.
Admitted.

(** Reuse previou lemmas (easy). *)
Lemma SOS_Psquare_round :
  forall n i, eqnatb i n = false ->
  SOS (Inter (Psquare n) (invar_cc i)) (Inter (Psquare n) (invar_cc (S i))).
Proof.
Admitted.

(** Easy *)
Theorem SOS_Psquare_n_end :
  forall n, SOS (Inter (Psquare n) (invar_cc n)) (Final (invar_cc n)).
Proof.
Admitted.

Theorem SOS_Psquare_2_end_V2 : SOS (Inter Psquare_2 [0;0;1]) (Final [2;4;5]).
Proof.
  eapply SOS_trans.
  { apply SOS_Psquare_round. reflexivity. }
  eapply SOS_trans.
  { apply SOS_Psquare_round. reflexivity. }
  eapply SOS_trans.
  { apply SOS_Psquare_n_end. }
  apply SOS_stop.
Qed.

(** We can get information on the version that loops endlessly. *)
Lemma SOS_Psquare_inf_round :
  forall i,
  SOS (Inter Psquare_inf (invar_cc i)) (Inter Psquare_inf (invar_cc (S i))).
Proof.
Admitted.

Theorem SOS_Psquare_inf_i :
  forall i,
  SOS (Inter Psquare_inf [0; 0; 1]) (Inter Psquare_inf (invar_cc i)).
Proof.
Admitted.

(** State and prove the general theorem for [Psquare] (****) *)
(**
  This part is more difficult, here are some hints interspersed with
  QUESTIONS (numbered [Psquare_Q1], [Psquare_Q2], etc.,
  with a number of stars corresponding to the difficulty)
  to be answerd.

  First you have to clearly understand the meaning of [SOS_Psquare_inf_i].
  The same theorem can be stated using (Psquare 0), (Psquare 1), (Psquare 2)
  or more generally (Psquare n) in the place of [Psquare_inf].
  For example :

Theorem SOS_Psquare_2_i :
  forall i,
  SOS (Inter Psquare_inf [0; 0; 1]) (Inter (Psquare 2) (invar_cc i)).

Theorem SOS_Psquare_n_i :
  forall n i,
  SOS (Inter Psquare_inf [0; 0; 1]) (Inter (Psquare n) (invar_cc i)).

These statements are actually too greedy to hold, for example
[SOS_Psquare_2_i] can be proved for [i] equal to 0, 1, 2 but not beyond.

* QUESTION Psquare_Q1 ( ** ): explain why.

A right statement for [SOS_Psquare_n_i] would be:
Lemma SOS_Psquare_n_i_le :
  forall n i, i <= n ->
  SOS (Inter (Psquare n) [0; 0; 1]) (Inter (Psquare n) (invar_cc i)).

* QUESTION Psquare_Q2 ( ** ): what we are interested in, at the end, 
is a theorem generalizing [SOS_Psquare_2_end_V1], relating the final state
reached by (Psquare n). State it, and explain why, intuitively,
it should be a consequence of [SOS_Psquare_n_i] (still unproven at the moment).

[SOS_Psquare_n_i] is provable, but this requires some training with
the <= (less or equal) relation.

We propose instead two possible tricks.
You can try one or the other (or both!).

A/ The first trick consists in replacing the use of <= by an addition.
Indeed, [i <= n] is equivalent to say that [n] is in the form [i + d]
for some [d], because our integers, in particular [d], are actually 
natural numbers.
The idea is then to reformulate a statement enonce in the form
[forall n i, i <= n ->  P n i]
as
[forall i d, (i + d) i.]

* QUESTION Psquare_Q3 ( * ) : reformulate the statement [SOS_Psquare_n_i_le]:
Lemma SOS_Psquare_n_plus : COMPLETΕ HERE.

* QUESTION Psquare_Q4 ( **** many proof techniques presented in previous
  lectures are useful here):
prove [SOS_Psquare_n_i_plu]s


* QUESTION Psquare_Q5 ( ** ) :
Prove the theorem announced in question [Psquare_Q2].
Hint: state first an auxiliary lemma relating only to variable [n], 
expressing that configuration [Inter (Psquare n) (invar_cc n)] 
can be reached from the initial configuration.

B/ The second possible trick has nothing to do with arithmetics.
The idea consists in replacing [SOS_Psquare_n_i] by a disjunction that
turns out to be provable:
Lemma SOS_Psquare_n_i_disj :
  forall n i,
    SOS (Inter (Psquare n) [0; 0; 1]) (Inter (Psquare n) (invar_cc i)) \/
    SOS (Inter (Psquare n) [0; 0; 1]) (Inter (Psquare n) (invar_cc n)).

In the course of the proof, [n] remains fixed.
Schematiqcally [i] is incremented by 1 starting from 0, and at each
round an equlity test between [i] and [n] is performed.

* QUESTION Psquare_Q6 ( *** ):
Write in your native language the proof of [SOS_Psquare_n_i_disj],
using a reasoning by case on the disjunctive hypothesis.
Fo example, given a hypothesis or a known theorem [Dis : A \/ B],
stating that either we have (a proof of) [A] or (a proof of) [B].
" We reson by case on [Dis].
  - either we have [A]
    (reasoning concluding to [C], using [A])
  - or we have [B]
    (reasoning concluding to [C], using [B])
  Then [C] is proved."

And to prove a disjunction [A \/ B], it is enough to prove [A]
or to prove [B] (with a suitable choice among [A] or [B]).

Easy exercise for a preliminary training:
prove [B \/ A] from [A \/ B].

In Coq those proof principles are implemented by the following tactics:
- reasoning by case: tactic [destruct], as usual.
  The above proof model would be implemented by: 
  destruct Dis as [HA | HB].
- to prove [A \/ B] when we choose to prove [A] : tactic [left].
-  to prove [A \/ B] hen we choose to prove [B] : tactic [right].

* QUESTION Psquare_Q7 (easy training in Coq): prove
Lemma or_commut : forall (A B : Prop), A \/ B -> B \/ A.

* QUESTION Psquare_Q8 (short but *** ):
  prove [SOS_Psquare_n_i_disj] in Coq.
To prove the equality  between [i] and [n], you can use
[case_eq (eqnatb i n)].

* QUESTION Psquare_Q9 ( * ) : deduce a lemma relating only to [n],
then the desired theorem on the final state reached by [Psquare n].

*)

(* ========================================================================== *)


(** * II *)


(** ** Define a functional version of [SOS_1] *)
Fixpoint f_SOS_1 (i : winstr) (s : state) : config.
Admitted.

(** ** Use [f_SOS_1] in order to avoid [eapply SOS_again] *)

(** CP = checkpoint *)
Definition CP0 := Psquare_2.
Eval cbn in (f_SOS_1 CP0 [0;0;1]).

(** The code has to be deconstructed in order to exhibit checkpoints. *)

Definition CP2 := Seq body_square CP0.
Definition CP1 := If (Bnot (Beqnat Ir (Aco 2))) CP2 Skip.

(** Those checkpoints allow a condensed writing of the
    configurations of interest. *)

(** We check the progress. *)
Fact fa1 : f_SOS_1 CP0 [0;0;1] = Inter CP1 [0;0;1]. Admitted. (* reflexivity. Qed. *)
Eval cbn in (f_SOS_1 CP1 [0;0;1]).
(** Move on, we fall back on [CP0] after some steps. *)

(** Use on a [SOS] lemma *)
(** The following proof must no longer use [eapply], bu instead
    [apply... with CCC]
    where [CCC] stands for a configuration that was guessed using [f_SOS_1]. *)
Lemma SOS_Psquare_2_1st_round_V1 :
  SOS (Inter Psquare_2 [0;0;1]) (Inter Psquare_2 [1; 1; 3]).
Proof.
  change Psquare_2 with CP0.
  apply SOS_again with (Inter CP1 [0;0;1]).
  { apply SOS1_While. }
Admitted.

(** ** General theorems relating [SOS_1] with [f_SOS_1]. *)

(** Short but non trivial. *)
Lemma f_SOS_1_corr : forall i s, SOS_1 i s (f_SOS_1 i s).
Proof.
Admitted.

(** Short. Warning: use tactic [injection]. *)
Lemma f_SOS_1_compl : forall i s c, SOS_1 i s c -> c = f_SOS_1 i s.
Proof.
Admitted.