(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)


(* Contribution to the Coq Library   V6.3 (July 1999)                    *)

(* ---                           develop.v                              --- *)
(*                                                                          *)
(* Author: Pierre Casteran.                                                 *)
(*    LABRI, URA CNRS 1304,                                                 *)
(*    Departement d'Informatique, Universite Bordeaux I,                    *)
(*    33405 Talence CEDEX,                                                  *)
(*    e-mail:  casteran@labri.u-bordeaux.fr                                 *)

(* 

  This file contains some important lemmas used in the "generation" module.
  It tells how to compose abstract machine code (with append) to build
  code for Call_M, Call_C and Call_K calls (see the module "spec")
*)

Require Import Constants.
Require Import monoid.
Require Import spec.
Require Import machine.
Require Import Wf_compl.
Require Import Plus.
Require Import Mult.
Require Import Lt.
Require Import Mult_compl.
Require Import euclid.
Require Import two_power.


(* A sequence for computing the cube of some m in M *)
Lemma M3 : gencode (Call_M three).
(******************************)
Proof.
(* Goal: gencode (Call_M three) *)
 refine (gencode_intro _ (seq PUSH (seq SQR (seq MUL End))) _).
(*
 Realizer (seq PUSH (seq SQR (seq MUL End))).
 Program_all. 
*)
(* Goal: Spec (Call_M p) c *)
 constructor 1.
(* Goal: forall (M : Set) (MO : monoid M) (a : M) (s : Stack M), @eq (Config M) (Exec M MO (seq PUSH (seq SQR (seq MUL End))) (config M a s)) (config M (power M MO a three) s) *)
 simpl in |- *; unfold power, three in |- *; intros.
(* Goal: @eq (Config M) (config M (o M MO (o M MO a a) a) s) (config M (o M MO a (o M MO a (o M MO a (u M MO)))) s) *)
 rewrite (u_neutral_r M MO).
(* Goal: @eq (Config M) (config M (o M MO (o M MO a a) a) s) (config M (o M MO a (o M MO a a)) s) *)
 rewrite <- (point_assoc M MO); auto with arith.
 Qed.




(* A sequence for computing the (2^q)-th power of some m in M;
 this is a sequence of q SQRs  *)



Lemma M2q : forall q : nat, gencode (Call_M (two_power q)).
(**********************************************)
Proof.
 refine
  (let t := fun q : nat => gencode (Call_M (two_power q)) in
   (fix M2q (q : nat) : t q :=
      match q as x return (t x) with
      | O => gencode_intro _ End _
      | S p =>
          match M2q p with
          | gencode_intro c s => gencode_intro _ (seq SQR c) _
          end
      end)).
(* 
 Realizer [q:nat]<Code>Match q with End
                                    ([_,c:?](seq SQR c))
                                    end.
 Program_all.
*)
(* Goal: Spec (Call_M p) c *)
 constructor 1.
(* Goal: forall (M : Set) (MO : monoid M) (a : M) (s : Stack M), @eq (Config M) (Exec M MO End (config M a s)) (config M (power M MO a (two_power O)) s) *)
(* Goal: Spec (Call_M (two_power (S p))) (seq SQR c) *)
 unfold power in |- *; simpl in |- *.
(* Goal: forall (M : Set) (MO : monoid M) (a : M) (s : Stack M), @eq (Config M) (config M a s) (config M (o M MO a (u M MO)) s) *)
(* Goal: Spec (Call_M (two_power (S p))) (seq SQR c) *)
 intros; rewrite (u_neutral_r M MO); auto with arith.
(* Goal: Spec (Call_M (two_power (S p))) (seq SQR c) *)
 constructor 1; auto with arith.
(* Goal: forall (M : Set) (MO : monoid M) (a : M) (s : Stack M), @eq (Config M) (Exec M MO (seq SQR c) (config M a s)) (config M (power M MO a (two_power (S p))) s) *)
 intros; simpl in |- *.
(* Goal: @eq (Config M) (Exec M MO c' (Exec M MO c (config M a s1))) (config M (power M MO a (Nat.mul q p)) s1) *)
 inversion_clear s.
(* Goal: @eq (Config M) (Exec M MO c' (Exec M MO c (config M a s1))) (config M (power M MO a (Nat.mul q p)) s1) *)
 rewrite H.
(* Goal: @eq (Config M) (config M (power M MO (power M MO a p) q) (push M (power M MO a p) s)) (config M (power M MO a (Nat.mul q p)) (push M (power M MO a p) s)) *)
 apply Config_inv; auto with arith.
(* Goal: @eq M (power M MO (o M MO a a) (two_power p)) (power M MO a (Nat.add (two_power p) (Nat.add (two_power p) O))) *)
 rewrite <- plus_n_O.
(* Goal: @eq M (power M MO (o M MO a a) (two_power p)) (power M MO a (Nat.add (two_power p) (two_power p))) *)
 apply a2x; auto with arith.
Qed.


(* code generation  for (Call_M p) from the code for (Call_C p q) 
   (it's the same!) *)

Lemma C2M : forall p q : nat, gencode (Call_C p q) -> gencode (Call_M p).
(****************************************)
Proof.
 refine
  (fun p q g => match g with
                | gencode_intro c s => gencode_intro _ c _
                end).
(*
 Realizer [p,q:nat][c:Code]c.
 Program_all.
*)
(* Goal: Spec (Call_M p) c *)
 constructor 1.
(* Goal: @eq (Config M) (Exec M MO c' (Exec M MO c (config M a s1))) (config M (power M MO a (Nat.mul q p)) s1) *)
 inversion_clear s.
(* Goal: @eq (Config M) (config M (o M MO (power M MO (power M MO a p) q) (power M MO a r)) (push M (power M MO a p) s)) (config M (power M MO a (Nat.add (Nat.mul q p) r)) (push M (power M MO a p) s)) *)
 auto with arith.
Qed.



(*  code generation for  (Call_C qp p) from the codes for (Call_M p) and (Call_M q)
    just append !                                                          *)
Lemma MMC :
 forall p q : nat,
 gencode (Call_M p) -> gencode (Call_M q) -> gencode (Call_C (q * p) p).
(***********************************************)
Proof.
 refine
  (fun p q g g' =>
   match g with
   | gencode_intro c s =>
       match g' with
       | gencode_intro c' s0 => gencode_intro _ (app c c') _
       end
   end).
(*
 Realizer [p,q:nat][c,c':Code](app c  c').
 Program_all.
*)
(* Goal: Spec (Call_C (Nat.add (Nat.mul q p) r) p) (app cpr (app cq (seq MUL End))) *)
 constructor 2.
(* Goal: forall (M : Set) (MO : monoid M) (a : M) (s : Stack M), @eq (Config M) (Exec M MO (app kpr (seq PUSH (seq SWAP (app mq (seq MUL End))))) (config M a s)) (config M (power M MO a (Nat.add (Nat.mul q p) r)) (push M (power M MO a p) s)) *)
 intros; rewrite Exec_app.
(* Goal: @eq (Config M) (Exec M MO c' (Exec M MO c (config M a s1))) (config M (power M MO a (Nat.mul q p)) s1) *)
 inversion_clear s.
(* Goal: @eq (Config M) (Exec M MO c' (Exec M MO c (config M a s1))) (config M (power M MO a (Nat.mul q p)) s1) *)
 rewrite H.
(* Goal: @eq (Config M) (Exec M MO c' (config M (power M MO a p) s1)) (config M (power M MO a (Nat.mul q p)) s1) *)
 inversion_clear s0.
(* Goal: @eq (Config M) (Exec M MO c' (config M (power M MO a p) s1)) (config M (power M MO a (Nat.mul q p)) s1) *)
 rewrite (H0 M MO).
(* Goal: @eq (Config M) (config M (o M MO (power M MO (power M MO a p) q) (power M MO a r)) (push M (power M MO a p) s)) (config M (power M MO a (Nat.add (Nat.mul q p) r)) (push M (power M MO a p) s)) *)
 rewrite power_mult; auto with arith.
Qed.


(* code generation for  (Call_C qp+r p) from cpr (code for (Call_K p r))
                                      and cq (code for (Call_M q))   
 (it's cpr, followed by cq then a MUL statement                       *)

Lemma KMC :
 forall p q r : nat,
 gencode (Call_K p r) -> gencode (Call_M q) -> gencode (Call_C (q * p + r) p).
(***********************************************************)
Proof.
 refine
  (fun p q r g g' =>
   match g with
   | gencode_intro cpr s =>
       match g' with
       | gencode_intro cq s0 =>
           gencode_intro _ (app cpr (app cq (seq MUL End))) _
       end
   end).
(*
 Realizer [p,q,r:nat][cpr,cq:Code](app cpr (app  cq (seq MUL   End))).
 Program_all.
*)
(* Goal: @eq (Config M) (Exec M MO c' (config M (power M MO a p) s1)) (config M (power M MO a (Nat.mul q p)) s1) *)
 inversion_clear s; inversion_clear s0.
(* Goal: Spec (Call_C (Nat.add (Nat.mul q p) r) p) (app cpr (app cq (seq MUL End))) *)
 constructor 2.
(* Goal: forall (M : Set) (MO : monoid M) (a : M) (s : Stack M), @eq (Config M) (Exec M MO (app kpr (seq PUSH (seq SWAP (app mq (seq MUL End))))) (config M a s)) (config M (power M MO a (Nat.add (Nat.mul q p) r)) (push M (power M MO a p) s)) *)
 intros; rewrite Exec_app.
(* Goal: @eq (Config M) (Exec M MO (app cq (seq MUL End)) (Exec M MO cpr (config M a s))) (config M (power M MO a (Nat.add (Nat.mul q p) r)) s) *)
 rewrite (H M MO a).
(* Goal: @eq (Config M) (Exec M MO (app cq (seq MUL End)) (config M (power M MO a p) (push M (power M MO a r) s))) (config M (power M MO a (Nat.add (Nat.mul q p) r)) s) *)
 rewrite (Exec_app M MO); simpl in |- *; rewrite H0.
(* Goal: @eq (Config M) (Exec1 M MO MUL (config M (power M MO (power M MO a p) q) (push M (power M MO a r) s))) (config M (power M MO a (Nat.add (Nat.mul q p) r)) s) *)
 simpl in |- *.
(* Goal: @eq (Config M) (config M (o M MO (power M MO (power M MO a p) q) (power M MO a r)) s) (config M (power M MO a (Nat.add (Nat.mul q p) r)) s) *)
 apply Config_inv.
(* Goal: @eq (Config M) (config M (o M MO (power M MO (power M MO a p) q) (power M MO a r)) (push M (power M MO a p) s)) (config M (power M MO a (Nat.add (Nat.mul q p) r)) (push M (power M MO a p) s)) *)
 rewrite power_eucl; auto with arith.
(* Goal: @eq (Config M) (config M (o M MO (power M MO (power M MO a p) q) (power M MO a r)) (push M (power M MO a p) s)) (config M (power M MO a (Nat.add (Nat.mul q p) r)) (push M (power M MO a p) s)) *)
 auto with arith.
Qed.


(* Code generation for (Call_K qp p) from cp (code for (Call_M p))
                                   and cq (code for (Call_M q))
   It's cp, followed by a PUSH, then cq                       *)

Lemma MMK :
 forall p q : nat,
 gencode (Call_M p) -> gencode (Call_M q) -> gencode (Call_K (q * p) p).
(**************************************************)
Proof.
 refine
  (fun p q g g' =>
   match g with
   | gencode_intro cp s =>
       match g' with
       | gencode_intro cq s0 => gencode_intro _ (app cp (seq PUSH cq)) _
       end
   end).
(* 
 Realizer [p,q:nat][cp,cq:Code](app cp  (seq PUSH  cq)).
 Program_all. 
*)
(* Goal: @eq (Config M) (Exec M MO c' (config M (power M MO a p) s1)) (config M (power M MO a (Nat.mul q p)) s1) *)
 inversion_clear s; inversion_clear s0.
(* Goal: Spec (Call_K (Nat.add (Nat.mul q p) r) p) (app kpr (seq PUSH (seq SWAP (app mq (seq MUL End))))) *)
 constructor 3.
(* Goal: forall (M : Set) (MO : monoid M) (a : M) (s : Stack M), @eq (Config M) (Exec M MO (app kpr (seq PUSH (seq SWAP (app mq (seq MUL End))))) (config M a s)) (config M (power M MO a (Nat.add (Nat.mul q p) r)) (push M (power M MO a p) s)) *)
 intros; rewrite Exec_app. 
(* Goal: @eq (Config M) (Exec1 M MO MUL (config M (power M MO (power M MO a p) q) (push M (power M MO a r) s))) (config M (power M MO a (Nat.add (Nat.mul q p) r)) s) *)
 rewrite H; simpl in |- *.
(* Goal: @eq (Config M) (Exec1 M MO MUL (config M (power M MO (power M MO a p) q) (push M (power M MO a r) s))) (config M (power M MO a (Nat.add (Nat.mul q p) r)) s) *)
 rewrite H0; simpl in |- *.
(* Goal: @eq (Config M) (config M (power M MO (power M MO a p) q) (push M (power M MO a p) s)) (config M (power M MO a (Nat.mul q p)) (push M (power M MO a p) s)) *)
 apply Config_inv; auto with arith.
(* Goal: @eq (Config M) (config M (o M MO (power M MO (power M MO a p) q) (power M MO a r)) (push M (power M MO a p) s)) (config M (power M MO a (Nat.add (Nat.mul q p) r)) (push M (power M MO a p) s)) *)
 rewrite <- power_mult; auto with arith.
Qed.


(* Code generation for (Call_K qp+r p) from kpr (code for (Call_K p r))
                                     and mq (code for (Call_M q))
  it's kpr, followed by a sequence (PUSH;SWAP), then mq and a MUL statement *)

Lemma KMK :
 forall p q r : nat,
 gencode (Call_K p r) -> gencode (Call_M q) -> gencode (Call_K (q * p + r) p).
(***********************************************************)
Proof.
  refine
   (fun p q r g g' =>
    match g with
    | gencode_intro kpr s =>
        match g' with
        | gencode_intro mq s0 =>
            gencode_intro _
              (app kpr (seq PUSH (seq SWAP (app mq (seq MUL End))))) _
        end
    end).
(*
 Realizer [p,q,r:nat][kpr,mq:Code]
    (app kpr  (seq PUSH (seq  SWAP  ( app mq  (seq MUL  End))))).
 Program_all.
*)
(* Goal: @eq (Config M) (Exec M MO c' (config M (power M MO a p) s1)) (config M (power M MO a (Nat.mul q p)) s1) *)
 inversion_clear s; inversion_clear s0.
(* Goal: Spec (Call_K (Nat.add (Nat.mul q p) r) p) (app kpr (seq PUSH (seq SWAP (app mq (seq MUL End))))) *)
 constructor 3.
(* Goal: forall (M : Set) (MO : monoid M) (a : M) (s : Stack M), @eq (Config M) (Exec M MO (app kpr (seq PUSH (seq SWAP (app mq (seq MUL End))))) (config M a s)) (config M (power M MO a (Nat.add (Nat.mul q p) r)) (push M (power M MO a p) s)) *)
 intros; rewrite Exec_app.
(* Goal: @eq (Config M) (Exec1 M MO MUL (config M (power M MO (power M MO a p) q) (push M (power M MO a r) s))) (config M (power M MO a (Nat.add (Nat.mul q p) r)) s) *)
 rewrite H; simpl in |- *.
(* Goal: @eq (Config M) (Exec M MO (app mq (seq MUL End)) (config M (power M MO a p) (push M (power M MO a r) (push M (power M MO a p) s)))) (config M (power M MO a (Nat.add (Nat.mul q p) r)) (push M (power M MO a p) s)) *)
 rewrite Exec_app.
(* Goal: @eq (Config M) (config M (o M MO (power M MO (power M MO a p) q) (power M MO a r)) (push M (power M MO a p) s)) (config M (power M MO a (Nat.add (Nat.mul q p) r)) (push M (power M MO a p) s)) *)
 rewrite H0; simpl in |- *. auto with arith.
(* Goal: @eq (Config M) (config M (o M MO (power M MO (power M MO a p) q) (power M MO a r)) (push M (power M MO a p) s)) (config M (power M MO a (Nat.add (Nat.mul q p) r)) (push M (power M MO a p) s)) *)
 rewrite power_eucl; auto with arith.
Qed.







