Cookies disclaimer

I agree Our site saves small pieces of text information (cookies) on your device in order to deliver better content and for statistical purposes. You can disable the usage of cookies by changing the settings of your browser. By browsing our website without changing the browser settings you grant us permission to store that information on your device.

[2019-Jul] XOR

Xorbert has a sequence of bits. He has some odd obsession which asks him to know for a subsequence of the given sequence whether there is an odd number of 1's in it. Weird, right?

Every now and then his brain wants to have the result for a subsequence starting at some position s and ending at position e. His left half of the brain is busy with some other mathematical problem, so he asks you to write an efficient extension to his brain that can answer those queries quickly. Efficient obviously means linear time!

More formal: we have some input i :: (nat => bool) representing the sequence of bits. And you are provided a task triple: that is two sequences of start index (si :: nat => nat) and end indices (ei :: nat => nat) as well as N - the length of the input sequence. Your task is to fill a final sequence (f :: nat => bool) where the yth entry of f is True iff there is an odd number of 1's in the input sequence between indices (si y) and (ei y).

Your computation model is the following:

Give a function that maps an task triple to a list of commands that solves the task. The last part of the triple is N: the number of elements from the sequence we look at and also the number of query tuples (s,e) you get. Your generated plan must be linear in N.

You can get partial points for XOR_interval, XOR_odd_odd and GOAL. Just sorry/admit the goals you can not prove.

Resources

Download Files

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
Download Files

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.
Download Files

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
Download Files

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

Terms and Conditions