[2019-Jul] XOR

Definitions File

Require Export Arith Lia.
Require Import ssreflect ssrbool.
Require Export List.
Export ListNotations.

(*** xor *)

Definition xor (x y: bool): bool :=
  match x with
  | true => negb y
  | false => y
  end.

Lemma xor_com x y : xor x y = xor y x.
Proof. destruct x; destruct y; reflexivity. Qed.

Lemma xor_assoc x y z : xor x (xor y z) = xor (xor x y) z.
Proof. destruct x; destruct y; destruct z; reflexivity. Qed.

Lemma xor_same x : xor x x = false.
Proof. destruct x; reflexivity. Qed.

Lemma xor_false_r x : xor x false = x.
Proof. destruct x; reflexivity. Qed.
Lemma xor_false_l x : xor false x = x.
Proof. destruct x; reflexivity. Qed.
Lemma xor_true_l x : xor x true = negb x.
Proof. reflexivity. Qed.
Lemma xor_true_r x : xor true x = negb x.
Proof. reflexivity. Qed.

(* Can be used by ssreflect's rewrite to rewrite with any of the lemmas in the
   tuple: use "rewrite xorE" *)
Definition xorE := (xor_same, xor_false_r, xor_false_l, xor_true_l, xor_true_r).

(*** XOR: iterated xor *)

(* The list of natural numbers from i (included) to j (excluded) *)
Notation "'[' i '..<' j ']'" := (seq i (j-i)) (only parsing).

(* Useful lemma when reasoning by induction on [i..<j], ie on (j-i). *)
Lemma seq_length_S start len : seq start (S len) = seq start len ++ [start+len].
Proof.
  revert start. induction len; intros start.
  - rewrite //= Nat.add_0_r //.
  - rewrite //=. f_equal.
    rewrite -{1}seq_shift -map_cons. cbn [seq] in IHlen.
    rewrite IHlen map_app //= Nat.add_succ_r -seq_shift //.
Qed.

Lemma interval_app x y z:
  x <= y -> y <= z ->
  [x..<y] ++ [y..<z] = [x..<z].
Proof.
  intros Hxy Hyz.
  set n := z - y. rewrite (_:z = y+n) //. unfold n. lia.
  induction n.
  - rewrite //= app_nil_r Nat.add_0_r //.
  - rewrite (_:y + S n - x = S(y+n-x)) //. lia.
    rewrite !seq_length_S app_assoc IHn //=.
    rewrite (_: x + (y + n - x) = y + n) //=. lia.
Qed.

Definition XOR i j f :=
  fold_right (fun x n => xor n (f x)) false [i..<j].

Lemma bubble_foldr_xor (f: nat -> bool) xs y z :
  xor (fold_right (fun x n => xor n (f x)) y xs) z =
  fold_right (fun x n => xor n (f x)) (xor y z) xs.
Proof.
  revert y z. induction xs. reflexivity.
  intros y z. rewrite //= -IHxs -!xor_assoc (xor_com z) //.
Qed.

Lemma XOR_same x i : XOR x x i = false.
Proof. rewrite /XOR Nat.sub_diag /seq //. Qed.

Lemma XOR_cons x y f :
  x <= y ->
  XOR x (S y) f = xor (XOR x y f) (f y).
Proof.
  intro. rewrite /XOR. rewrite Nat.sub_succ_l //.
  rewrite seq_length_S fold_right_app //= -le_plus_minus //.
  rewrite bubble_foldr_xor xorE //=.
Qed.

(* Helpers to work on sequences represented as functions (nat -> A) *)

Definition update {A} (seq: nat -> A) (k: nat) (v: A): nat -> A :=
  fun n => if Nat.eq_dec k n then v else seq n.

Notation "f '{' k := v '}'" := (update f k v) (at level 0).

Lemma update_read_neq A (seq: nat -> A) k k' v :
  k <> k' ->
  seq {k:=v} k' = seq k'.
Proof.
  intros Hk. rewrite /update. destruct (Nat.eq_dec k k'); cbn.
  now exfalso; auto. auto.
Qed.

Lemma update_read_eq A (seq: nat -> A) k k' v :
  k = k' ->
  seq {k:=v} k' = v.
Proof.
  intros Hk. rewrite /update. destruct (Nat.eq_dec k k'); cbn.
  auto. now exfalso; auto.
Qed.

(*** Computational model *)

(* input sequence: nth number is odd iff (i n) is true *)
Notation input := (nat -> bool) (only parsing).

(* output sequence (is part of the state defined below) *)
Notation output := (nat -> bool) (only parsing).

Record state := State {
  (* Temporary memory that can be read/written by the program *)
  tmp : nat -> bool;

  (* Registers: can be xor'd together, or loaded with data from the input or
  temporary memory *)
  regA : bool;
  regB : bool;

  (* Output, is written by the program *)
  out : output;
}.

(* Program instructions *)
Variant Com :=
  | LoadIA of nat
  | LoadIB of nat
  | Xor
  | StoreTmp of nat
  | StoreFinal of nat
  | LoadTA of nat
  | LoadTB of nat.

(* Semantics of program instructions *)

Definition exec (i: input) (s: state) (c: Com): state :=
  match c with
  | LoadIA n =>
    (* LoadIA n : A <- i(n) *)
    {| tmp := tmp s; regA := i n; regB := regB s; out := out s |}
  | LoadIB n =>
    (* LoadIB n : B <- i(n) *)
    {| tmp := tmp s; regA := regA s; regB := i n; out := out s |}
  | LoadTA n =>
    (* LoadTA n : A <- tmp(n) *)
    {| tmp := tmp s; regA := tmp s n; regB := regB s; out := out s |}
  | LoadTB n =>
    (* LoadTB n : B <- tmp(n) *)
    {| tmp := tmp s; regA := regA s; regB := tmp s n; out := out s |}
  | Xor =>
    (* Xor : A <- xor A B *)
    {| tmp := tmp s; regA := xor (regA s) (regB s); regB := regB s; out := out s |}
  | StoreTmp n =>
    (* StoreTmp n : tmp(n) <- A *)
    {| tmp := (tmp s){n := regA s}; regA := regA s; regB := regB s; out := out s |}
  | StoreFinal n =>
    (* StoreFinal n : out(n) <- A *)
    {| tmp := tmp s; regA := regA s; regB := regB s; out := (out s){n := regA s} |}
  end.

Definition execs (i: input) (s: state) (cs: list Com): state :=
  fold_left (exec i) cs s.

Lemma execs_app i s cs cs' : execs i s (cs ++ cs') = execs i (execs i s cs) cs'.
Proof. rewrite /execs fold_left_app //=. Qed.


(** Definitions for the correctness statement *)

(* A given program solves a specific task *)

Record task := Task {
  (* the size of the relevant input prefix *)
  size : nat;
  (* start indices *)
  si : nat -> nat;
  (* end indices *)
  ei : nat -> nat;

  (* start and end indices are valid: they fall below the size *)
  si_lt_ei : forall n, n < size -> si n < ei n;
  ei_inbound : forall n, n < size -> ei n < size;
}.

Definition number_of_true_between x y i :=
  length (filter i [x..<y]).

Definition correct_solution (t: task) (i: input) (o: output) :=
  forall x, x < size t ->
  o x = Nat.odd (number_of_true_between (si t x) (ei t x) i).

Definition correct_solution_XOR (t: task) (i: input) (o: output) :=
  forall x, x < size t ->
  o x = XOR (si t x) (ei t x) i.

Template File

Require Import Defs.

(* It is not required, but it is a good idea to import ssreflect to benefit
   from the better rewrite tactic. (by uncommenting the two lines below)

   ssreflect's rewrite cheatsheet: a rewrite invocation is of the form [rewrite foo bar baz],
   where each of "foo", "bar", "baz" can be:
   - "foo" where foo is a lemma: rewrites with the lemma ("-foo" rewrites in the other direction)
   - "!foo" where foo is a lemma: rewrites repeatedly with foo
   - "/foo" where foo is a definition: unfolds the definition ("-/foo" folds the definition)
   - "//": try to prove the goal or side-condition if it is trivial
   - "//=": like "//" but also simplify the goal (using "simp")
   - "(_: foo = bar)": ask the user to prove "foo = bar" as a subgoal, and rewrite with it
*)

(*
Require Import ssreflect ssrbool.
Ltac done ::= first [ solve [ trivial | auto | lia ] ].
*)

(** Part 1 -- properties of XOR *)

(* a few useful lemmas: *)
Lemma xor_shuffle a b c : xor a b = c <-> xor a c = b.
Proof.
  (* todo *)
Admitted.

Check bubble_foldr_xor.
(* forall (f : output) (xs : list nat) (y z : bool),
     xor (fold_right (fun (x : nat) (n : bool) => xor n (f x)) y xs) z =
     fold_right (fun (x : nat) (n : bool) => xor n (f x)) (xor y z) xs *)

Check seq_length_S.
(* forall start len : nat,
     seq start (S len) = seq start len ++ [start + len]
*)

Check interval_app.
(* forall x y z : nat,
     x <= y -> y <= z ->
     [x..<y] ++ [y..<z] = [x..<z]
*)

Lemma XOR_interval x y f:
  x <= y ->
  xor (XOR 0 x f) (XOR 0 y f) = XOR x y f.
Proof.
  (* todo *)
Admitted.

(** Part 2: number_of_true_between reduction to XOR *)

Lemma XOR_odd_odd x y f: XOR x y f = Nat.odd (number_of_true_between x y f).
Proof.
  (* todo *)
Admitted.

Lemma reduction (t: task) (i: input) (o: output):
  correct_solution_XOR t i o ->
  correct_solution t i o.
Proof.
  (* todo *)
Admitted.

(** Part 3 -- Implementation time! *)

Theorem goal :
  exists (prog: task -> list Com),
    (* functional correctness *)
    (forall (t: task) (s0: state) (i: input),
      correct_solution t i (out (execs i s0 (prog t))))
    /\
    (* complexity: linear in the size of the task *)
    (exists (n0 c: nat), forall t, n0 <= size t -> length (prog t) <= c * (size t)).
Proof.
  (* todo *)
Admitted.

Definitions File

theory Defs
imports Main
begin

section \<open>xor\<close>

fun xor (infixr "<>" 64) where
  "xor True True = False"
| "xor True False = True"
| "xor False True = True"
| "xor False False = False"
 
lemma xor_com: "a <> b = b <> a "
  by(cases a; cases b; auto)

lemma xor_assoc: "a <> b <> c = (a <> b) <> c"
  by(cases a; cases b; cases c; auto)

lemma xor_same[simp]: "a <> a = False"
  by(cases a;  auto)

lemma xor_False[simp]: "a <> False = a"
  by(cases a; auto) 
lemma xor_False2[simp]: "False <> a = a"
  by(cases a; auto)  
lemma xor_True: "a <> True = (\<not> a)"
  by(cases a; auto)  
lemma xor_True2: "True <> a = (\<not> a)"
  by(cases a; auto)  
 

section \<open>XOR\<close>

definition XOR where "XOR i j f = foldr (\<lambda>x n. n <> (f x)) [i..<j] False"  

value "XOR 0 6 (%_. True)"
value "XOR 0 0 (%_. True)"
value "XOR 0 1 (%n. (if n = 0 then a else True))"

lemma XOR_same[simp]: "XOR x x i = False"
  apply(auto simp: XOR_def) done


lemma bubble_foldr_xor:
  "xor (foldr (\<lambda>x n. n <> (f x)) xs y) z
            = foldr (\<lambda>x n. n <> (f x)) xs (y <> z)"
  apply (induct "xs" arbitrary: y z)
  subgoal by auto
  subgoal apply simp
    apply(subst xor_assoc[symmetric]) 
    apply(subst xor_assoc[symmetric]) 
    apply(subst (3) xor_com) by simp
  done 

lemma XOR_Suc: "x\<le>y \<Longrightarrow> XOR x (Suc y) i = (XOR x y i) <> (i y)"
  apply (simp add: XOR_def)
    apply(subst bubble_foldr_xor) by simp

section \<open>Computational model\<close>

type_synonym input = "(nat \<Rightarrow> bool)"
type_synonym task = "(nat \<Rightarrow> nat) \<times> (nat \<Rightarrow> nat)  \<times> nat"
type_synonym state = "( (nat\<Rightarrow>bool) \<times> bool \<times> bool \<times> (nat\<Rightarrow>bool))"

datatype Com = LoadIA nat | LoadIB nat | Xor | StoreTmp nat | StoreFinal nat |
                  LoadTA nat | LoadTB nat

fun exec :: "input \<Rightarrow> state \<Rightarrow> Com \<Rightarrow> state"  where
   "exec i (tmp,a,b,f) (LoadIA n) = (tmp,i n,b,f)"
|  "exec i (tmp,a,b,f) (LoadIB n) = (tmp,a,i n,f)"
|  "exec i (tmp,a,b,f) (LoadTA n) = (tmp,tmp n,b,f)"
|  "exec i (tmp,a,b,f) (LoadTB n) = (tmp,a,tmp n,f)"
|  "exec i (tmp,a,b,f) (Xor) = (tmp,a <> b,b,f)"
|  "exec i (tmp,a,b,f) (StoreTmp n) = (tmp(n:=a),a,b,f)" 
|  "exec i (tmp,a,b,f) (StoreFinal n) = (tmp,a,b,f(n:=a))" 

fun execs where
  "execs i s [] = s"
|  "execs i s (c#cs) = execs i (exec i s c) cs"

lemma execs_append:
  "execs i s (as@bs) = execs i (execs i s as) bs"
  by (induct as arbitrary: s bs) simp_all


definition "output = (\<lambda>(_,_,_,f). f)"

definition "tasksize = (\<lambda>(_,_,N). N)" 
 

section \<open>the Task\<close>

definition "number_of_true_between x y i = length (filter i [x..<y])"


definition correct_solution where
  "correct_solution i = (\<lambda>(si,ei,n) f. (\<forall>x<n. f x = odd (number_of_true_between (si x) (ei x) i) ))"


definition correct_solution_XOR where
  "correct_solution_XOR i  = (\<lambda>(si,ei,n) f. (\<forall>x<n. f x = XOR (si x) (ei x) i ))"

 

end

Template File

theory Submission
imports Defs
begin


section \<open>Part 1 - Stuff about XOR\<close>
 
(* a hint: *)

lemma xor_shuffle: "a <> b = c \<longleftrightarrow> a <> c = b"
  apply(cases a; cases b; cases c) by auto

thm bubble_foldr_xor

lemma upt_append_continuous: "x\<le>y \<Longrightarrow> [0..<x] @ [x..<y] = [0..<y]"  
  by (metis le0 le_iff_add upt_add_eq_append)


(* a partial goal *)

lemma XOR_interval: \<comment> \<open>gives 1/4 point\<close>
  "x\<le>y \<Longrightarrow> (XOR 0 x i) <> (XOR 0 y i) = (XOR x y i)"
  sorry

section \<open>Part 2 - number_of_true_between reduction to XOR (1/4 point)\<close>
 

lemma XOR_odd_odd: \<comment> \<open>gives 1/4 point\<close>
  "XOR x y i = odd (number_of_true_between x y i)"
  sorry


lemma reduction:
  assumes "(\<forall>x<n. si x < ei x \<and> ei x < n)"
  shows
 "correct_solution_XOR i (si,ei,n) s
      \<Longrightarrow> correct_solution i (si,ei,n) s" 
  using assms by(auto simp: correct_solution_XOR_def correct_solution_def XOR_odd_odd) 
 


section \<open>Part 3 - Solution: ALGORITHM (1/2 point)\<close>
 

lemma GOAL:   \<comment> \<open>gives 1/2 point\<close>
  shows "\<exists>f:: task \<Rightarrow> Com list.
      \<forall>i si ei N s. 
      (\<forall>x<N. si x < ei x \<and> ei x < N) \<longrightarrow> 
            \<comment> \<open>functional correctness\<close>
             correct_solution i (si,ei,N) (output (execs i s (f (si,ei,N))))
         \<and>
            \<comment> \<open>complexity: linear in the size of the task\<close>
             (\<exists>n0 c:: nat. \<forall>t. n0 \<le> tasksize t \<longrightarrow> length (f t) \<le> c * (tasksize t))"
  sorry




end

Check File

theory Check
imports Submission
begin

 
lemma GOAL1: "x\<le>y \<Longrightarrow> (XOR 0 x i) <> (XOR 0 y i) = (XOR x y i)"
    apply(rule Submission.XOR_interval) by simp

lemma GOAL2: "XOR x y i = odd (number_of_true_between x y i)"
  by(rule Submission.XOR_odd_odd) 

lemma GOAL3: 
  shows "\<exists>f:: task \<Rightarrow> Com list.
      \<forall>i si ei N s. 
      (\<forall>x<N. si x < ei x \<and> ei x < N) \<longrightarrow> 
            \<comment> \<open>functional correctness\<close>
             correct_solution i (si,ei,N) (output (execs i s (f (si,ei,N))))
         \<and>
            \<comment> \<open>complexity: linear in the size of the task\<close>
             (\<exists>n0 c:: nat. \<forall>t. n0 \<le> tasksize t \<longrightarrow> length (f t) \<le> c * (tasksize t))"
  apply(rule Submission.GOAL) done




end

Definitions File

theory Defs
imports Main
begin

section \<open>xor\<close>

fun xor (infixr "<>" 64) where
  "xor True True = False"
| "xor True False = True"
| "xor False True = True"
| "xor False False = False"
 
lemma xor_com: "a <> b = b <> a "
  by(cases a; cases b; auto)

lemma xor_assoc: "a <> b <> c = (a <> b) <> c"
  by(cases a; cases b; cases c; auto)

lemma xor_same[simp]: "a <> a = False"
  by(cases a;  auto)

lemma xor_False[simp]: "a <> False = a"
  by(cases a; auto) 
lemma xor_False2[simp]: "False <> a = a"
  by(cases a; auto)  
lemma xor_True: "a <> True = (\<not> a)"
  by(cases a; auto)  
lemma xor_True2: "True <> a = (\<not> a)"
  by(cases a; auto)  
 

section \<open>XOR\<close>

definition XOR where "XOR i j f = foldr (\<lambda>x n. n <> (f x)) [i..<j] False"  

value "XOR 0 6 (%_. True)"
value "XOR 0 0 (%_. True)"
value "XOR 0 1 (%n. (if n = 0 then a else True))"

lemma XOR_same[simp]: "XOR x x i = False"
  apply(auto simp: XOR_def) done


lemma bubble_foldr_xor:
  "xor (foldr (\<lambda>x n. n <> (f x)) xs y) z
            = foldr (\<lambda>x n. n <> (f x)) xs (y <> z)"
  apply (induct "xs" arbitrary: y z)
  subgoal by auto
  subgoal apply simp
    apply(subst xor_assoc[symmetric]) 
    apply(subst xor_assoc[symmetric]) 
    apply(subst (3) xor_com) by simp
  done 

lemma XOR_Suc: "x\<le>y \<Longrightarrow> XOR x (Suc y) i = (XOR x y i) <> (i y)"
  apply (simp add: XOR_def)
    apply(subst bubble_foldr_xor) by simp

section \<open>Computational model\<close>

type_synonym input = "(nat \<Rightarrow> bool)"
type_synonym task = "(nat \<Rightarrow> nat) \<times> (nat \<Rightarrow> nat)  \<times> nat"
type_synonym state = "( (nat\<Rightarrow>bool) \<times> bool \<times> bool \<times> (nat\<Rightarrow>bool))"

datatype Com = LoadIA nat | LoadIB nat | Xor | StoreTmp nat | StoreFinal nat |
                  LoadTA nat | LoadTB nat

fun exec :: "input \<Rightarrow> state \<Rightarrow> Com \<Rightarrow> state"  where
   "exec i (tmp,a,b,f) (LoadIA n) = (tmp,i n,b,f)"
|  "exec i (tmp,a,b,f) (LoadIB n) = (tmp,a,i n,f)"
|  "exec i (tmp,a,b,f) (LoadTA n) = (tmp,tmp n,b,f)"
|  "exec i (tmp,a,b,f) (LoadTB n) = (tmp,a,tmp n,f)"
|  "exec i (tmp,a,b,f) (Xor) = (tmp,a <> b,b,f)"
|  "exec i (tmp,a,b,f) (StoreTmp n) = (tmp(n:=a),a,b,f)" 
|  "exec i (tmp,a,b,f) (StoreFinal n) = (tmp,a,b,f(n:=a))" 

fun execs where
  "execs i s [] = s"
|  "execs i s (c#cs) = execs i (exec i s c) cs"

lemma execs_append:
  "execs i s (as@bs) = execs i (execs i s as) bs"
  by (induct as arbitrary: s bs) simp_all


definition "output = (\<lambda>(_,_,_,f). f)"

definition "tasksize = (\<lambda>(_,_,N). N)" 
 

section \<open>the Task\<close>

definition "number_of_true_between x y i = length (filter i [x..<y])"


definition correct_solution where
  "correct_solution i = (\<lambda>(si,ei,n) f. (\<forall>x<n. f x = odd (number_of_true_between (si x) (ei x) i) ))"


definition correct_solution_XOR where
  "correct_solution_XOR i  = (\<lambda>(si,ei,n) f. (\<forall>x<n. f x = XOR (si x) (ei x) i ))"

 

end

Template File

theory Submission
imports Defs
begin


section \<open>Part 1 - Stuff about XOR\<close>
 
(* a hint: *)

lemma xor_shuffle: "a <> b = c \<longleftrightarrow> a <> c = b"
  apply(cases a; cases b; cases c) by auto

thm bubble_foldr_xor

lemma upt_append_continuous: "x\<le>y \<Longrightarrow> [0..<x] @ [x..<y] = [0..<y]"  
  by (metis le0 le_iff_add upt_add_eq_append)


(* a partial goal *)

lemma XOR_interval: \<comment> \<open>gives 1/4 point\<close>
  "x\<le>y \<Longrightarrow> (XOR 0 x i) <> (XOR 0 y i) = (XOR x y i)"
  sorry

section \<open>Part 2 - number_of_true_between reduction to XOR (1/4 point)\<close>
 

lemma XOR_odd_odd: \<comment> \<open>gives 1/4 point\<close>
  "XOR x y i = odd (number_of_true_between x y i)"
  sorry


lemma reduction:
  assumes "(\<forall>x<n. si x < ei x \<and> ei x < n)"
  shows
 "correct_solution_XOR i (si,ei,n) s
      \<Longrightarrow> correct_solution i (si,ei,n) s" 
  using assms by(auto simp: correct_solution_XOR_def correct_solution_def XOR_odd_odd) 
 


section \<open>Part 3 - Solution: ALGORITHM (1/2 point)\<close>
 

lemma GOAL:   \<comment> \<open>gives 1/2 point\<close>
  shows "\<exists>f:: task \<Rightarrow> Com list.
      \<forall>i si ei N s. 
      (\<forall>x<N. si x < ei x \<and> ei x < N) \<longrightarrow> 
            \<comment> \<open>functional correctness\<close>
             correct_solution i (si,ei,N) (output (execs i s (f (si,ei,N))))
         \<and>
            \<comment> \<open>complexity: linear in the size of the task\<close>
             (\<exists>n0 c:: nat. \<forall>t. n0 \<le> tasksize t \<longrightarrow> length (f t) \<le> c * (tasksize t))"
  sorry




end

Check File

theory Check
imports Submission
begin

 
lemma GOAL1: "x\<le>y \<Longrightarrow> (XOR 0 x i) <> (XOR 0 y i) = (XOR x y i)"
    apply(rule Submission.XOR_interval) by simp

lemma GOAL2: "XOR x y i = odd (number_of_true_between x y i)"
  by(rule Submission.XOR_odd_odd) 

lemma GOAL3: 
  shows "\<exists>f:: task \<Rightarrow> Com list.
      \<forall>i si ei N s. 
      (\<forall>x<N. si x < ei x \<and> ei x < N) \<longrightarrow> 
            \<comment> \<open>functional correctness\<close>
             correct_solution i (si,ei,N) (output (execs i s (f (si,ei,N))))
         \<and>
            \<comment> \<open>complexity: linear in the size of the task\<close>
             (\<exists>n0 c:: nat. \<forall>t. n0 \<le> tasksize t \<longrightarrow> length (f t) \<le> c * (tasksize t))"
  apply(rule Submission.GOAL) done




end