From dd77e9267808f15ed10cf8f52a39323485b7cb52 Mon Sep 17 00:00:00 2001 From: Dominique Larchey-Wendling Date: Tue, 28 Mar 2023 12:39:51 +0200 Subject: [PATCH] typo --- BOWLING.md | 60 ---- HANOI.md | 33 -- bowling.v | 790 ------------------------------------------- hanoi.v | 656 ----------------------------------- sort.v | 159 --------- sorting_algorithms.v | 6 +- 6 files changed, 3 insertions(+), 1701 deletions(-) delete mode 100644 BOWLING.md delete mode 100644 HANOI.md delete mode 100644 bowling.v delete mode 100644 hanoi.v delete mode 100644 sort.v diff --git a/BOWLING.md b/BOWLING.md deleted file mode 100644 index 5f58c50..0000000 --- a/BOWLING.md +++ /dev/null @@ -1,60 +0,0 @@ -# Modeling Bowling plays and scores - -## Goal of the project - -The goal of the project is to model the _scoring_ in the [game of -bowling](https://fr.wikipedia.org/wiki/Bowling). -Ultimately, we show that the score of a bowling play is a natural number -between 0 (minimum score) and 300 (maximum score) and that every score -from 0 to 300 can be realized by at least one bowling play. - -## Quick informal description of the scoring in bowling - -One bowling play is composed of -* _10 initial frames_ of one or two _rolls_ cumulating up to 10 _pins_ down: - - strictly less than 10 pins down give an _open_ frame, example 7+2; - - 10 pins down in two rolls give a _spare_, example 9+1 or 0+10; - - and 10 pins down on the first roll give a _strike_. In that case, - there is no second roll; -* (possibly) _one extra frame_ composed of one or two rolls. - In case of two rolls, if the first roll strikes 10, then - 10 new pins are made available for the second roll. - -To count the score, one counts the total of pins down in the -10 initial frames. But spares and strikes get extra pin value: -* on a spare, the pins down on the following roll is counted - as extra on the spare. For example, a spare 9+1 followed - by a open frame 5+3 counts as 9+1+5; -* on a strike, the pins down on the two following rolls are - counted as extra on the strike. For example, a strike followed - by a strike and a open frame 3+6 counts as 10+10+3. -* the reason for the existence of the extra frame is to complete the score of - the last (or two last) initial frames, if they are spares - or strikes. - -## The code source code to complete the project - -The standalone Coq source file [`bowling.v`](bowling.v) contains -code to achieve this modeling up to the characterization of realizable -scores. Your goal is to _fill the holes._ -Holes are totally `Admitted` or partially `admit`ted proof scripts. -The proof sketch will lead you to the goal. - -* You do not need to invent complicated inductions or introduce - new notions, the modeling is done for you; -* But you need to be able to understand how the informal problem - is modeled by these definitions and notations; -* Your capacity to use and combine tactics will be critical - to your success in filling proof holes; -* Some holes are very easy, and some other are more difficult; -* For those willing to go further, some suggested improvements - appear at the end of the project file. - -## Expectations and Timetable - -The project starts March 28th 2022 and lasts 6 weeks. It is an -**individual project** and students will be required to send a -completed project file to me [Dominique Larchey-Wendling](mailto:larchey@loria.fr) -after that six week period has expired. The deadline for sending the -completed project file is **May 6, 2022**. Please contact me if you have -any question or difficulty regarding the project. diff --git a/HANOI.md b/HANOI.md deleted file mode 100644 index e398b4c..0000000 --- a/HANOI.md +++ /dev/null @@ -1,33 +0,0 @@ -# Modeling and proving the Towers of Hanoi - -## Goal of the project - -The goal of the project is to model the game of -the [Towers of Hanoi](https://en.wikipedia.org/wiki/Tower_of_Hanoi). -Ultimately, we show that the well know recursive sequence of moves -is correct, ie. it can displace a full tower from the left rod/tower -to the right rod/tower, using the middle rod/tower as temporary storage. - -The standalone Coq source file [`hanoi.v`](hanoi.v) contains -code to achieve this outcome. Your goal is to _fill the holes._ -Holes are totally admitted or partially admitted proof scripts. -The proof sketch will lead you to the goal. - -* You do not need to invent complicated inductions or introduce - new notions, the modeling is done for you; -* But you need to be able to understand how the informal problem - is modeled by these definitions and notations; -* Your capacity to use and combine tactics will be critical - to your success in filling proof holes; -* Some holes are very easy, and some other are much more difficult; -* For those willing to go further, some suggested improvements - appear at the end of the project file. - -## Expectations and Timetable - -The project starts April 12th 2021 and lasts one month. It is an -**individual project** and students will be required to send a -completed project file to me [Dominique Larchey-Wendling](mailto:larchey@loria.fr) -after that one month period has expired. The deadline for sending the -completed project file is **May 17, 2021**. Please contact me if you have -any question or difficulty regarding the project. diff --git a/bowling.v b/bowling.v deleted file mode 100644 index 9a86944..0000000 --- a/bowling.v +++ /dev/null @@ -1,790 +0,0 @@ -(**************************************************************) -(* Copyright Dominique Larchey-Wendling [*] *) -(* *) -(* [*] Affiliation LORIA -- CNRS *) -(**************************************************************) -(* This file is distributed under the terms of the *) -(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *) -(**************************************************************) - -Require Import Arith Lia List Euclid. - -Import ListNotations. - -(** The tactic "destr n up to i as H" the generates the (i+1) subgoals: - - n is 0 - - n is 1 - - n is ... - - n is i-1 - - H: i <= n -*) - -Fact lt_le_dec m n : { n < m } + { m <= n}. -Proof. destruct (le_lt_dec m n); auto. Qed. - -(* Generates cases x is 0, ... x is i-1, and x is (S ... S ..)*) -Ltac destruct_up_to x i := - match i with - | 0 => try lia - | S ?i => destruct x as [ | x ]; [ | destruct_up_to x i ] - end. - -(* Generates cases x is 0, ..., x is i-1 and H:i <= x *) -Tactic Notation "destr" ident(n) "up" "to" constr(i) "as" ident(H) := - destruct (lt_le_dec i n) as [ H | H ]; [ destruct_up_to n i; clear H | ]. - -Tactic Notation "destr" ident(n) "up" "to" constr(i) := - let H := fresh in destr n up to i as H. - -(* Example of use of the tactic destr _ up to _ as _*) -Goal forall n, n = 0 \/ n = 1 \/ 2 <= n. -Proof. - intros n. - destr n up to 2 as Hn. - + auto. (* subgoal n is 0 *) - + auto. (* subgoad n is 1 *) - + auto. (* subgoal Hn : 2 <= n *) -Qed. - -(** Reversed (right to left) notations for lists *) - -Local Notation "l '-:' x" := (cons x l) (at level 59, left associativity, format "l -: x") : list_scope. -Local Notation "l ':-:' m" := (app m l) (at level 59, left associativity, format "l :-: m") : list_scope. - -Local Notation "[ x ]" := ([]-:x) : list_scope. -(* Local Notation "[ x ⊳ .. ⊳ y ⊳ z ]" := (( .. ([] -: x) .. -: y) -: z ) : list_scope. *) - -Local Reserved Notation "x ↑ n" (at level 50, left associativity, format "x ↑ n"). - -(** The repeater: x↑n = [ x ⊳ x ⊳ ... ⊳ x ] where x is repeated n times *) -Fixpoint repeat {X} (x : X) n := - match n with - | 0 => [] - | S n => x↑n -: x - end -where "x ↑ n" := (repeat x n). - -Fact repeat_S X (x : X) n : x↑(S n) = x↑n -: x. -Proof. reflexivity. Qed. - -(** Sum of a list of natural numbers *) -Fixpoint lsum l := - match l with - | [] => 0 - | l -: x => x+lsum l - end. - -(** Some useful arithmetic inequalities *) -Local Fact lt_0_10 : 0 < 10. Proof. lia. Qed. -Local Fact lt_1_10 : 1 < 10. Proof. lia. Qed. -Local Fact le_0_10 : 0 <= 10. Proof. lia. Qed. -Local Fact lt_9_10 : 9 < 10. Proof. lia. Qed. - -Section Bowling. - - (** Reserved Notations for the Bowling game predicates *) - - Reserved Notation "l '//' m '-[' n ']->' s" (at level 70, format "l // m -[ n ]-> s"). - Reserved Notation "'I||-' x '@' y '>>'" (at level 70, format "I||- x @ y >>"). - Reserved Notation " l '+:' e '-->' s" (at level 70, format "l +: e --> s"). - Reserved Notation "'B||-' x" (at level 70, format "B||- x"). - - (** Modelling the Bowling plays with frames, rolls, pins down etc *) - - (* The (first ten) initial bowling frames - - OPN/open: 2 rolls, no strike, no spare - SPA/spare: 2 rolls, first roll < 10 pins down, - second roll completes to 10 pins - STR/strike: 1 roll, 10 pins down - - *) - - Inductive iframe : Type := - | open a b : a + b < 10 -> iframe (* a pins on 1st roll, b pins on second roll *) - | spare a : a < 10 -> iframe (* a pins on 1st roll, 10-a on second roll *) - | strike : iframe (* 10 pins on first roll, no second roll *) - . - - Notation OPN := open. - Notation SPA := spare. - Notation STR := strike. - - (* empty frame, with zero pins down *) - Definition ZERO := (OPN 0 0 lt_0_10). - - (* The list of pins down for each roll of an initial frame *) - Definition iframe2pins r := - match r with - | OPN a b _ => [a;b] - | SPA a _ => [a;10-a] - | STR => [10] - end. - - Arguments iframe2pins r /. - - (* Value (number of pins down) of the first ball of a frame *) - Definition ifirst r := - match r with - | OPN a _ _ => a - | SPA a _ => a - | STR => 10 - end. - - Arguments ifirst r /. - - (* ifirst matches the first roll of iframe2pins *) - Fact ifirst_eq_first_pin r : - match iframe2pins r with - | [] => False - | x::_ => ifirst r = x - end. - Proof. destruct r; reflexivity. Qed. - - (* Total of pins down of an initial frame *) - Definition itotal r := - match r with - | OPN a b _ => a + b - | SPA _ _ => 10 - | STR => 10 - end. - - Arguments itotal r /. - - (* itotal matches the sum of pins in iframe2pins *) - Fact itotal_eq_sum_pins r : itotal r = lsum (iframe2pins r). - Proof. destruct r; simpl itotal; unfold iframe2pins, lsum; lia. Qed. - - (* The extra bowling frame, one or two rolls to complete - pending strikes or spares - - EX0: zero extra roll - EX1: one extra roll to complete a spare - EX2: two extra rolls to complete one (or two) strike(s) - - Notice than if the first roll of EX2 is 10 pins down (ie strike), - then a new set of 10 pins is made available for the second roll - *) - - Inductive eframe : Type := - | extra0 : eframe (* no extra roll *) - | extra1 a : a <= 10 -> eframe (* only one extra roll *) - | extra2 a b : (a < 10 /\ a+b <= 10 (* no strike on first extra roll *) - \/ a = 10 /\ b <= 10) (* strike on the first roll, 10 new pins *) - -> eframe. - - Notation ER0 := extra0. - Notation ER1 := extra1. - Notation ER2 := extra2. - - (* The list of pins down for each roll of an extra frame *) - Definition eframe2pins e := - match e with - | ER0 => [] - | ER1 a _ => [a] - | ER2 a b _ => [a;b] - end. - - (* Status of the previous or two previous frames, if any *) - Inductive status := - | status_none (* the previous frame does not exist, or is open *) - | status_spare (* the last frame was a spare *) - | status_strike (* the last frame was a strike, but the one before, was not *) - | status_2strikes (* the last two frames were strikes *) - . - - Notation SNON := status_none. - Notation SSPA := status_spare. - Notation S1ST := status_strike. - Notation S2ST := status_2strikes. - - (* New status from previous status after an initial frame *) - Definition next_status (st : status) (r : iframe) := - match st, r with - | S1ST , STR => S2ST (* strike after a strike *) - | S2ST , STR => S2ST (* strike after two strikes *) - | _ , STR => S1ST (* strike after not a strike *) - | _ , SPA _ _ => SSPA (* spare after anything *) - | _ , OPN _ _ _ => SNON (* open frame after anything *) - end. - - Arguments next_status st r /. - - (* Pins down to add depending on the status of the two previous frames *) - Definition status_count st r := - match st with - | SNON => 0 (* nothing to add here *) - | SSPA => ifirst r (* count the first roll value on the previous frame *) - | S1ST => itotal r (* count the two rolls value on the previous frame *) - | S2ST => ifirst r+itotal r (* count the first roll on the two previous frames - plus the second on the previous frame *) - end. - - Arguments status_count st r /. - - Notation NXT := next_status. - Notation STC := status_count. - Notation TOT := itotal. - - Fact next_status_OPN st a b H : NXT st (OPN a b H) = SNON. - Proof. - Admitted. - - Fact next_status_ZERO st : NXT st ZERO = SNON. - Proof. - Admitted. - - Fact status_count_ZERO st : status_count st ZERO = 0. - Proof. - Admitted. - - (* The initial frames of a bowling play predicate: - - - l: list of frames - - st: status according to the last two frames - - n: number of frames - - sc : score so far - - l // st -[n]-> sc denotes - - "given the n many initial frames stored in the - list l, with current status st, the score is sc" - - defined by two inductive rules: - - ----------------------- empty play (zero frame) - [] // SNON -[0]-> 0 - - l // st -[n]-> sc - --------------------------------------------------- (n<10) next frame is r - l-:r // NXT st r -[1+n]-> STC st r + TOT r + sc - - *) - - Inductive frames : list iframe -> status -> nat -> nat -> Prop := - | frames_start : - - (*---------------------*) - [] // SNON -[0]-> 0 - - | frames_next l st n sc r : - - n < 10 -> l // st -[n]-> sc - (*---------------------------------------------------*) - -> l-:r // NXT st r -[1+n]-> STC st r + TOT r + sc - - where "l // st -[ n ]-> sc" := (frames l st n sc). - - Tactic Notation "play" "from" constr(st) := - match goal with - | |- _-:?r // _ -[ _ ]-> _ => apply (frames_next _ st _ _ r) - end; simpl; auto; try lia. - - (* Any sequence of frames of length <= 10 is valid: - if the length of l is below 10 then one can compute - a status st, and a score sc such that - l // st -[length l]-> sc *) - - Theorem frames_is_total l : - length l <= 10 - -> { st : _ & { sc | l // st -[length l]-> sc } }. - Proof. - induction l as [ | r l IHl ]; simpl; intros Hl. - + exists SNON, 0; constructor. - + destruct IHl as (st & sc & Hsc); try lia. - destruct r as [ a b H | a H | ]. - * exists SNON; destruct st. - - exists (a+b+sc); play from SNON. - - admit. - - admit. - - admit. - * exists SSPA. admit. - * admit. - Admitted. - - (** A backward fixpoint computation of the score for a list of frames - iscore [ r1 ⊳ r2 ⊳ ... ⊳ r10 ] a b - - l = [ r1 ⊳ r2 ⊳ ... ⊳ r10 ] - (a,b) = extra frame, 0 if no roll - - iscore l a b = score of l considering next to 2 rolls are [a; b] - - iscore [ r1 ⊳ r2 ⊳ ... ⊳ ri ⊳ (u,v) ] a b - = extra + u+v + iscore [ r1 ⊳ r2 ⊳ ... ⊳ ri ] u v - - where extra is - - 0 if (u,v) is open - - a if (u,v) is a spare and - - a+b if (u,_) is a strike - *) - - Fixpoint iscore l (a b : nat) := - match l with - | [] => 0 - | l-:OPN u v _ => u+v + iscore l u v - | l-:SPA u _ => a + 10 + iscore l u (10-u) - | l-:STR => a+b + 10 + iscore l 10 a - end. - - Fact iscore_fix l r a b : - iscore (l -: r) a b - = match r with - | OPN u v _ => u+v+iscore l u v - | SPA u _ => a+10+iscore l u (10-u) - | STR => a+b+10+iscore l 10 a - end. - Proof. reflexivity. Qed. - - Theorem frames_iscore l st n sc a b : - l // st -[n]-> sc - -> iscore l a b - = match st with - | SNON => 0 - | SSPA => a - | S1ST => a+b - | S2ST => 2*a+b - end + sc. - Proof. - intros H; revert H a b. - induction 1 as [ | l st n sc r Hn H IH ]; intros a b; auto. - rewrite iscore_fix. - revert IH; case_eq st; intros Est IH; (case_eq r; [intros u v Huv | intros u Hu | ]; intros Hr). - + simpl; rewrite IH; lia. - Admitted. - - Corollary frames_iscore_0 l st n sc : - l // st -[n]-> sc -> sc = iscore l 0 0. - Proof. - Admitted. - - Definition istatus l := - match l with - | _ -: STR -: STR => S2ST - | _ -: STR => S1ST - | _ -: SPA _ _ => SSPA - | _ => SNON - end. - - Theorem frames_istatus l st n sc : l // st -[n]-> sc -> st = istatus l. - Proof. - induction 1 as [ | l st n sc r Hn H IH ]; auto. - Admitted. - - Fact frames_length l st n sc : l // st -[n]-> sc -> n = length l. - Proof. - Admitted. - - Lemma frames_is_functional l st1 st2 n1 n2 sc1 sc2 : - l // st1 -[n1]-> sc1 - -> l // st2 -[n2]-> sc2 - -> n1 = n2 - /\ st1 = st2 - /\ sc1 = sc2. - Proof. - intros H1 H2. - rewrite frames_length with (1 := H1), - frames_istatus with (1 := H1), - frames_iscore_0 with (1 := H1). - Admitted. - - (* This theorem allows to prove a predicate l // st -[n]-> sc - by computation: from l, compute (length l), (iscore l 0 0) and - (istatus l) and verify the values match n, sc and st respectivelly *) - Theorem check_score l n st sc : - n <= 10 - -> n = length l - -> sc = iscore l 0 0 - -> st = istatus l - -> l // st -[n]-> sc. - Proof. - intros H1 H2 H3 H4. - destruct (frames_is_total l) as (st' & sc' & H5); try lia. - rewrite <- H2 in H5. - generalize (frames_iscore_0 _ _ _ _ H5) (frames_istatus _ _ _ _ H5). - intros; subst; auto. - Qed. - - Tactic Notation "check" "score" := - apply check_score; simpl; auto; lia. - - (** "score_reached st sc" denoted "I||- sc @ st >>" below - means: one can compute a list l of 10 initial frames - such that the score is sc after playing these 10 frames - of l, and the status is then st *) - - Definition score_reached_in st sc := { l | l // st -[10]-> sc }. - - Notation "I||- x @ y" := (score_reached_in y x) (at level 70). - - (** We describe how to get scores from 0 to 270 in - the 10 initial frames *) - - Section from_0_to_29. - - (* First the scores from 0 up to 29 *) - - Variable (sc : nat) (Hsc : sc < 10). - - Tactic Notation "frames" constr(l) := exists l; check score. - - (* How to get a score from 0 to 9 *) - Fact score_0_9 : I||- sc @ SNON. - Proof. frames ([OPN 0 sc Hsc] :-: ZERO↑9). Qed. - - (* How to get a score from 10 to 19 *) - Fact score_10_19 : I||- sc+10 @ SNON. - Proof. - Admitted. - - (* How to get a score from 20 to 29 *) - Fact score_20_29 : I||- sc+20 @ SNON. - Proof. - Admitted. - - End from_0_to_29. - - (* How to build scores up to 29 *) - Inductive sut29 : nat -> Type := - | sut29_1 : sut29 1 - | sut29_2 a b : a+b < 10 -> sut29 (3*a+2*b) - | sut29_3 n : 20 <= n < 30 -> sut29 n. - - (* Any score sc below 29 is either - - 1 - - or of the form 3a+b with a+b < 10 - - or in between 20 and 29 *) - Lemma score_up_to_30 sc : sc < 30 -> sut29 sc. - Proof. - intros Hsc. - destruct (eucl_dev 3) with (m := sc) - as [ q r Hr E ]; try lia. - destruct (le_lt_dec 20 sc) as [ H1 | H1 ]. - + constructor 3; lia. - + destr r up to 3. - * replace sc with (3*q+2*0) by lia. - constructor; lia. - * destruct q as [ | q ]. - - subst; simpl; constructor. - - replace sc with (3*q+2*2) by lia. - constructor; lia. - * replace sc with (3*q+2*1) by lia. - constructor; lia. - * lia. - Qed. - - Section from_30_to_270. - - (* Then the score from 30 up to 270 *) - - (* How to get score 30, 60, 90, ... 240 *) - Fact score_30n n : 1 <= n <= 8 -> I||- 30*n @ SNON. - Proof. - intros Hn. - exists (STR↑(1+n) :-: ZERO↑(9-n)). - destr n up to 9; simpl; check score. - Qed. - - (* How to get score 31 *) - Fact score_31 : I||- 31 @ SNON. - Proof. - Admitted. - - (* How to get score 61, 91, 121, ...., 241 *) - Fact score_30n_p1 n : 2 <= n <= 8 -> I||- 30*n+1 @ SNON. - Proof. - Admitted. - - (* How to get score 32-57, 62-87, 122-147, ... 242-267 *) - Fact score_30n_p2_27 n a b : 1 <= n <= 8 -> a+b < 10 -> I||- 30*n+3*a+2*b @ SNON. - Proof. - Admitted. - - (* How to get score 50-59, 80-89, ... 230-239 *) - Fact score_30n_p20_29 n a : 1 <= n <= 7 -> a < 10 -> I||- 30*n+20+a @ SNON. - Proof. - Admitted. - - (* How to get score 260-269 *) - Fact score_260_269 a : a < 10 -> I||- a+260 @ SSPA. - Proof. - Admitted. - - (* How to get score 270 *) - Fact score_270 : I||- 270 @ S2ST. - Proof. exists (STR↑10); check score. Qed. - - End from_30_to_270. - - (* How to build scores up to 270 *) - Inductive sut270 : nat -> Type := - | sut270_1 n a : n < 3 -> a < 10 -> sut270 (10*n+a) - | sut270_2 n : 1 <= n <= 8 -> sut270 (30*n+1) - | sut270_3 n a b : 1 <= n <= 8 -> a+b < 10 -> sut270 (30*n+3*a+2*b) - | sut270_4 n a : 1 <= n <= 7 -> a < 10 -> sut270 (30*n+20+a) - | sut270_5 a : a < 10 -> sut270 (260+a) - | sut270_6 : sut270 270. - - (* Any score below 270 is either - - of the form 10n+a with n < 3 and a < 10 - - of the form 30n+1 with 1 <= n <= 8 - - of the form 30n+3a+2b with 1 <= n <= 8 and a+b < 10 - - of the form 30n+20+a with 1 <= n <= 7 and a < 10 - - of the form 260+a with a < 10 - - 270 *) - Lemma score_up_to_270 sc : sc <= 270 -> sut270 sc. - Proof. - intros H1. - destruct (eucl_dev 30) with (m := sc) - as [ q r Hr E ]; try lia. - destruct (eq_nat_dec q 0) as [ H2 | H2 ]. - + subst; simpl. - destruct (eucl_dev 10) with (m := r) - as [ a n Hn E ]; try lia. - replace r with (10*a+n) by lia. - constructor; lia. - + destruct (eq_nat_dec q 9) as [ H3 | H3 ]. - * replace sc with 270 by lia; constructor 6. - * destruct score_up_to_30 with (1 := Hr) - as [ | a b | k ]. - - replace sc with (30*q+1) by lia. - constructor; lia. - - replace sc with (30*q+3*a+2*b) by lia. - constructor; lia. - - destruct (eq_nat_dec q 8) as [ H4 | H4 ]. - ++ replace sc with (260+(k-20)) by lia. - constructor; lia. - ++ replace sc with (30*q+20+(k-20)) by lia. - constructor; lia. - Qed. - - (** For any score below 270, one can compute a status st - such that <> is reached in the 10 initial frames *) - Theorem score_from_0_to_270 sc : sc <= 270 -> { st & I||- sc @ st }. - Proof. - intros H; apply score_up_to_270 in H. - destruct H as [ n a Hn Ha | n Hn | n a b Hn Hab | n a Hn Ha | a Ha | ]. - Admitted. - - Section frames_inversion_lemmas. - - Let frames_0 l st n sc : - l // st -[n]-> sc - -> n = 0 - -> sc = 0 - /\ st = SNON. - Proof. induction 1; auto; discriminate. Qed. - - Lemma frames_0_inv l st sc : - l // st -[0]-> sc - -> sc = 0 - /\ st = SNON. - Proof. Admitted. - - Let frames_1 l st n sc : - l // st -[n]-> sc - -> n = 1 - -> sc <= 10 - /\ st <> S2ST. - Proof. - induction 1 as [ | l st [] sc r H1 H3 _ ]; try discriminate; intros _. - apply frames_0 in H3 as (H3 & ->); auto. - destruct r; simpl; split; try (easy || lia). - Qed. - - Lemma frames_1_inv l st sc : - l // st -[1]-> sc - -> sc <= 10 - /\ st <> S2ST. - Proof. Admitted. - - Lemma frames_n_bound l st n sc : l // st -[n]-> sc -> n <= 10. - Proof. induction 1; lia. Qed. - - End frames_inversion_lemmas. - - Section the_maximum_score. - - (* We show that the maximum score after - - 0 frame is 0 - - 1 frame is 10 - - n>=2 frames is 30(n-1) *) - - Definition max_score n := - match n with - | 0 => 0 - | 1 => 10 - | S n => 30*n - end. - - Fact max_score_0 : max_score 0 = 0. Proof. reflexivity. Qed. - Fact max_score_1 : max_score 1 = 10. Proof. reflexivity. Qed. - - Fact max_score_ge_2 n : 2 <= n -> max_score n = 30*(n-1). - Proof. destruct n as [ | [] ]; simpl; lia. Qed. - - Fact max_score_S n : 2 <= n -> max_score (S n) = 30 + max_score n. - Proof. intros; rewrite !max_score_ge_2; lia. Qed. - - Lemma frames_score_bounded l st n sc : - l // st -[n]-> sc -> sc <= max_score n. - Proof. - induction 1 as [ | l st n sc r H1 H3 IH3 ]; auto. - destr n up to 2. - Check frames_0_inv. - Admitted. - - Theorem frames_score_max l st sc : l // st -[10]-> sc -> sc <= 270. - Proof. apply frames_score_bounded. Qed. - - End the_maximum_score. - - (** Definition of a bowling play: - - composed of 10 initial frames - - plus an extra (possibly empty) frame - - depending on the status of the last two rolls (status) - - A valid bowling play (l,e) of score sc is denoted - - l +: e --> sc - *) - - Inductive bowling : list iframe -> eframe -> nat -> Prop := - | bowling_none l sc : l // SNON -[10]-> sc -> l +: ER0 --> sc - | bowling_ext1 l sc a H : l // SSPA -[10]-> sc -> l +: ER1 a H --> a+sc - | bowling_ext2 l sc a b H : l // S1ST -[10]-> sc -> l +: ER2 a b H --> a+b+sc - | bowling_ext3 l sc a b H : l // S2ST -[10]-> sc -> l +: ER2 a b H --> 2*a+b+sc - where "l +: e --> s" := (bowling l e s). - - (* The list of pins down on each roll of a bowling play *) - Definition bowling2pins lr e := flat_map iframe2pins lr :-: eframe2pins e. - - (* For every initial 10 frames l scoring sc, one can compute an extra frame - e such that (l,e) constitute a bowling play of score sc - Notice that only scores below 270 can be reached that way *) - Lemma bowling_extends_rounds l st sc : - l // st -[10]-> sc -> { e | l +: e --> sc }. - Proof. - destruct st. - + exists ER0; constructor; auto. - Admitted. - - (** score computes the score correcly *) - Definition score l e := - match e with - | ER0 => iscore l 0 0 - | ER1 a _ => iscore l a 0 - | ER2 a b _ => iscore l a b - end. - - Theorem score_correct l e sc : l +: e --> sc -> sc = score l e. - Proof. - induction 1 as [ ? ? H | ? ? ? ? H | ? ? ? ? ? H | ? ? ? ? ? H ]. - Admitted. - - Lemma bowling_is_functional l e sc1 sc2 : - l +: e --> sc1 - -> l +: e --> sc2 - -> sc1 = sc2. - Proof. - intros H1 H2. - apply score_correct in H1. - apply score_correct in H2. - subst; auto. - Qed. - - (** "bowling_score sc" denoted "B||- sc" below - means one can compute - - a list l of initial frames - - and an extra frame e - which combined give the score sc *) - Definition bowling_score sc := - { lr : list iframe & { e : eframe | lr +: e --> sc } }. - - Notation "B||- x" := (bowling_score x). - - (* Score is bounded by 300 in the Bowling game *) - Theorem bowling_score_bounded sc : B||- sc -> sc <= 300. - Proof. - intros (l & e & H); revert H. - induction 1 as [ ? ? H | ? ? ? ? H | ? ? ? ? ? H | ? ? ? ? ? H ]. - + apply frames_score_max in H. lia. - Admitted. - - (** Let us show the converse: any score up to 300 is possible in Bowling *) - - Section from_0_to_270. - - Lemma initial_is_bowling_score st sc : I||- sc @ st -> B||- sc. - Proof. - intros (lr & H); exists lr. - apply bowling_extends_rounds with st; auto. - Qed. - - Corollary bowling_from_0_to_270 sc : sc <= 270 -> B||- sc. - Proof. - Admitted. - - End from_0_to_270. - - Section from_270_to_300. - - (* For any value n up to 30, there is an extra frame (ER2 a b _) such that n = 2a+b *) - Lemma from_0_to_30 n : n <= 30 -> { e | match e with ER2 a b _ => n = 2*a+b | _ => False end }. - Proof. - intros H1. - destruct (le_lt_dec 20 n) as [ H2 | H2 ]. - + eexists (ER2 10 (n-20) _); try lia. - + destruct (eucl_dev 2) with (m := n) - as [ q r Hr E ]; try lia. - eexists (ER2 q r _); lia. - Unshelve. - all: lia. - Qed. - - Lemma bowling_from_270_to_300 sc : 270 <= sc <= 300 -> B||- sc. - Proof. - intros Hsc. - destruct (from_0_to_30 (sc-270)) as (e & He); try lia. - exists (STR↑10), e. - Admitted. - - End from_270_to_300. - - (* Any score up to 300 can be reached by a bowling play *) - Theorem any_is_bowling_score sc : sc <= 300 -> B||- sc. - Proof. - intros Hs. - destruct (le_lt_dec sc 270). - Admitted. - - (** Remaing extra open questions, more difficult *) - - (* Show that scores from 1 to 280 can be realized with at least - two different bowling plays *) - Theorem more_than_one sc : - 1 <= sc <= 280 - -> exists lr1 e1 lr2 e2, - lr1 +: e1 --> sc - /\ lr2 +: e2 --> sc - /\ bowling2pins lr1 e1 <> bowling2pins lr2 e2. - Admitted. - - (* Show that for scores above 290, there is at most one - bowling play realizing the score *) - Theorem exactly_one sc lr1 e1 lr2 e2 : - 290 <= sc - -> lr1 +: e1 --> sc - -> lr2 +: e2 --> sc - -> bowling2pins lr1 e1 = bowling2pins lr2 e2. - Admitted. - - (** More complicated questions for those interested: - - show that 287 corresponds to two bowling plays - - characterize precisely the scores which correspond - to exactly one bowling play, which are those in the - set {0} U [288,300], ie either 0 or above 288. - - same question for those with two bowling plays - *) - -End Bowling. diff --git a/hanoi.v b/hanoi.v deleted file mode 100644 index ef8a0b3..0000000 --- a/hanoi.v +++ /dev/null @@ -1,656 +0,0 @@ -(**************************************************************) -(* Copyright Dominique Larchey-Wendling [*] *) -(* *) -(* [*] Affiliation LORIA -- CNRS *) -(**************************************************************) -(* This file is distributed under the terms of the *) -(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *) -(**************************************************************) - -Require Import List Permutation Arith Lia. - -Set Implicit Arguments. - -(** FOL equivalence lemmas *) - -Lemma exists_equiv X (P Q : X -> Prop) : (forall x, P x <-> Q x) -> ex P <-> ex Q. -Proof. -Admitted. - -Lemma exists_right X A (P : X -> Prop) : (exists x, A /\ P x) <-> A /\ ex P. -Proof. -Admitted. - -(** List related lemmas *) - -Section extra_list_results. - - Variable (A : Type). - - (* All variable names l[0-9]* have an implicit type *) - - Implicit Type l : list A. - - (* from l1++r1 = l2++r2, find the common factor - - Hint: by induction on l1 with generalized l2, - either l1 is shorter or l2 is shorter. - *) - - Lemma app_split l1 l2 r1 r2 : - l1++r1 = l2++r2 - -> exists m, l2 = l1++m /\ r1 = m++r2 - \/ l1 = l2++m /\ r2 = m++r1. - Proof. - revert l2; induction l1 as [ | a l1 IHl1 ]. - Admitted. - - (* A reverse induction principle for lists *) - - Section list_rev_ind. - - Variable (P : list A -> Prop) - (HP0 : P nil) - (HP1 : forall l a, P l -> P (l++a::nil)). - - Let P_rev : forall l, P (rev l). - Proof. - Admitted. - - (* Hint: l = rev (rev l) *) - - Theorem list_rev_ind l : P l. - Proof. - Admitted. - - End list_rev_ind. - -End extra_list_results. - -(** Compare the two induction principles *) - -Check list_ind. -Check list_rev_ind. - -(** Permutation related notation and tactics *) - -(* Infix notation l ~p m is shortcut for (Permutation l m) *) - -Infix "~p" := (@Permutation _) (at level 70, no associativity). - -(* Permutation tactic notations for goals - - perm comm right: k ~p l++m becomes k ~p m++l - perm skip: x::l ~p x::m becomes l ~p m - k++l ~p k++m becomes l ~p m - perm sym: l ~p m becomes m ~p l - perm assoc: rewrite goals according to associativity of ++ and :: - perm trans H: when H : l1 ~p l2, - l1 ~p m becomes l2 ~p m - perm incl: incl l m becomes l ~p m - -*) - -Tactic Notation "perm" "comm" "right" := - apply perm_trans with (2 := Permutation_app_comm _ _); simpl. - -Tactic Notation "perm" "skip" := - match goal with - | |- _::_ ~p _::_ => apply perm_skip - | |- ?l++_ ~p ?l++_ => apply Permutation_app_head - end. - -Tactic Notation "perm" "sym" := apply Permutation_sym. - -Tactic Notation "perm" "assoc" := repeat (rewrite !app_ass; simpl). - -Tactic Notation "perm" "trans" hyp(H) := - match type of H with - | ?l1 ~p ?l2 => - match goal with - | |- ?l1 ~p _ => apply perm_trans with (1 := H) - | |- _ ~p ?l1 => apply perm_trans with (2 := Permutation_sym H) - end - end. - -Tactic Notation "perm" "incl" := - let x := fresh in intro x; apply Permutation_in; clear x. - -(* Example of use of the permutation tactics *) - -Goal forall X l m (x : X), l++x::m ~p m++x::l. -Proof. - intros X l m x. - perm comm right. - perm sym. - perm comm right. - perm skip. - perm comm right. - perm skip. - auto. -Qed. - -(** Human friendly notation for lists: - - - x ∈ l : x is a member of l - - l ⊆ m : l is included in m - - ⌊l⌋ : the length of l - - The definitions are to be found in the List - module of the Standart Library - - *) - -Infix "∈" := In (at level 70, no associativity). -Infix "⊆" := incl (at level 70, no associativity). -Notation "⌊ l ⌋" := (length l) (at level 1, format "⌊ l ⌋"). - -Hint Resolve incl_refl incl_appl incl_appr : core. - -(** Strict sorted lists of nat(ural numbers) - - 1) slu (for strictly lower-upper) denoted infix l ⪻ r: - - every member of l is strictly below (<) every member of r - - 2) m is strictly sorted denoted prefix ↗ m: - - for any split m = l++r we have l ⪻ r - -*) - -Definition strict_lower_upper l r := forall x y, x ∈ l -> y ∈ r -> x < y. - -Infix "⪻" := strict_lower_upper (at level 70, no associativity). - -(** A possible definition of strictly increasing list - Exercise: provide alternate characterizations for strictly - increasing lists and show equivalence *) - -Definition si_list m := forall l r, m = l++r -> l ⪻ r. - -Notation "↗ m" := (si_list m) (at level 70). - -Section strict_lists. - - Implicit Type l m : list nat. - - (* ⪻ is decreasing in both arguments - Hint: Check for the definitions of In/∈ and incl/⊆ in the - List module. - *) - - Fact slu_dec l l' m m' : l ⊆ l' -> m ⊆ m' -> l' ⪻ m' -> l ⪻ m. - Proof. - Admitted. - - Fact slu_nil_l l : nil ⪻ l. - Proof. - Admitted. - - Fact slu_nil_r l : l ⪻ nil. - Proof. - Admitted. - - Hint Immediate slu_nil_l slu_nil_r : core. - - (* Equivalences for ⪻ wrt list operators ::, ++ *) - - (* case of singleton lists _::nil *) - - Fact slu_sg_l x l : x::nil ⪻ l <-> forall y, y ∈ l -> x < y. - Proof. - Admitted. - - Fact slu_sg_r x l : l ⪻ x::nil <-> forall y, y ∈ l -> y < x. - Proof. - Admitted. - - (* What about ⪻ and ++ - Hint: in_or_app, in_app_or, in_app_iff *) - - Fact slu_app_l l1 l2 r : l1++l2 ⪻ r <-> l1 ⪻ r /\ l2 ⪻ r. - Proof. - Admitted. - - Fact slu_app_r l r1 r2 : l ⪻ r1++r2 <-> l ⪻ r1 /\ l ⪻ r2. - Proof. - Admitted. - - (* What about ⪻ and ++ and exchange - Hint: rewrite using slu_app_[lr] *) - - Fact slu_xchg l1 l2 m : l1++m ⪻ l2 -> l1 ⪻ m -> l1 ⪻ m++l2. - Proof. - Admitted. - - (* What about ⪻ and insertion on the right - Hint: use "perm ..." tactics *) - - Fact slu_insert x m l1 l2 : m++x::nil ⪻ l1++l2 -> m ⪻ x::nil -> m ⪻ l1++x::l2. - Proof. - intros H1 H2. - apply slu_dec with (l' := m) (m' := (x::nil)++l1++l2); auto. - + perm incl. - admit. - + admit. - Admitted. - - (* Strictly increasing lists and list operators *) - - Fact si_list_nil : ↗ nil. - Proof. - Admitted. - - Fact si_list_one x : ↗ x::nil. - Proof. - Admitted. - - Hint Resolve si_list_nil si_list_one : core. - - (* Hint: app_ass, in_or_app, in_app_iff and the above app_split *) - - Fact si_list_app l r : ↗ l++r <-> ↗ l /\ ↗ r /\ l ⪻ r. - Proof. - Admitted. - - (* Hint: x::l = (x::nil)++l *) - - Fact si_list_cons x l : ↗ x::l <-> x::nil ⪻ l /\ ↗ l. - Proof. - Admitted. - -End strict_lists. - -Hint Resolve slu_nil_l slu_nil_r - si_list_nil si_list_one : core. - -(** Some reservations for upcoming notations, semantics described later on *) - -Reserved Notation "'£' s" (at level 1, format "£ s"). -Reserved Notation "s '#' t" (at level 1, no associativity, format "s # t"). - -Reserved Notation "l '[' t ']>' s" (at level 65, right associativity, format "l [ t ]> s"). - -Reserved Notation "x '~[' m ']~>' y '⟦' ld '⟧'" (at level 70, format "x ~[ m ]~> y ⟦ ld ⟧"). -Reserved Notation "x '~{' lm '}~>' y '⟦' ld '⟧'" (at level 70, format "x ~{ lm }~> y ⟦ ld ⟧"). - -Section Hanoi. - - (** We establish that the Hanoi strategy is a correct way to play - Towers of Hanoi: see https://en.wikipedia.org/wiki/Tower_of_Hanoi *) - - (* 3 indices for the towers of Hanoi, with a decidable equality *) - - Inductive tower : Type := t1 | t2 | t3. - - Definition tower_eq_dec (x y : tower) : { x = y } + { x <> y }. - Proof. - revert x y; intros [] []; - ( (left; reflexivity) - || (right; discriminate) ). - Defined. - - (* Given two towers, one can always find a different one *) - - Definition tower_other x y := - match (x,y) with - | (t1,t1) => t2 | (t1,t2) => t3 | (t1,t3) => t2 - | (t2,t1) => t3 | (t2,t2) => t1 | (t2,t3) => t1 - | (t3,t1) => t2 | (t3,t2) => t1 | (t3,t3) => t1 - end. - - (* tower_other x y is indeed neither x nor y *) - - Fact tower_other_spec_x : forall x y, tower_other x y <> x. - Proof. - Admitted. - - Fact tower_other_spec_y : forall x y, tower_other x y <> y. - Proof. - Admitted. - - Hint Resolve tower_other_spec_x - tower_other_spec_y : core. - - (* A disk is characterized by its positive integer size/diameter - A stack is a list of disks *) - - Notation disk := nat. - Notation stack := (list disk). - - (* The state of play is described by three stacks - furthermore satisfying coherence conditions described - later on *) - - Definition state : Type := (stack * stack * stack)%type. - - (* The empty state, denoted ℰ *) - - Definition st_empty : state := (nil,nil,nil). - - Notation ℰ := st_empty. - - (* Which disks stack on a given tower t in state s, denoted s#t *) - - Definition st_get_tower (s : state) t := - match s, t with - | (l,_,_), t1 => l - | (_,l,_), t2 => l - | (_,_,l), t3 => l - end. - - Notation "s # t" := (st_get_tower s t). - - (* state change by stacking l on a tower t: - l[t]>s denotes the state obtained - from state s by prefixing tower t - with a stack l *) - - Definition st_stack_tower (s : state) (t : tower) (l : stack) : state := - match s, t with - | (l1,l2,l3), t1 => (l++l1,l2,l3) - | (l1,l2,l3), t2 => (l1,l++l2,l3) - | (l1,l2,l3), t3 => (l1,l2,l++l3) - end. - - Notation "l [ t ]> s" := (st_stack_tower s t l). - - (* Collect all the disks in state s, denoted £s - The list £s is always considered upto permutation - equivalence ~p, ie it is viewed as a multiset *) - - Definition st_collect (s : state) := - match s with (l1,l2,l3) => l1++l2++l3 end. - - Notation "£ s" := (st_collect s). - - (* The disks in tower s#t are contained in £s *) - - Fact get_tower_incl s t : s#t ⊆ £s. - Proof. - Admitted. - - Hint Resolve get_tower_incl : core. - - (* If disks in l are smaller than all those in state s - then they are also smaller than those in s#t - - Hint: ⪻ is decreasing *) - - Lemma slu_collect s l t : l ⪻ £s -> l ⪻ s#t. - Proof. - Admitted. - - (* Disks from a state change *) - - Fact st_stack_tower_collect s t l : £(l[t]>s) ~p l++£s. - Proof. - Admitted. - - (* The nil state change *) - - Fact st_stack_tower_nil : forall s t, nil[t]>s = s. - Proof. - Admitted. - - (* State change twice on the same tower *) - - Fact st_stack_tower_app s t l r : - l[t]>r[t]> s = l++r[t]>s. - Proof. - Admitted. - - (* State changes on two different towers commute *) - - Fact st_stack_tower_comm s t t' l r : - t <> t' - -> l[t]>r[t']>s = r[t']>l[t]> s. - Proof. - Admitted. - - (* State change vs st_get_tower on the same tower *) - - Fact st_get_stack_tower_eq s t l t' : - t = t' -> (l[t]>s)#t' = l++s#t'. - Proof. - Admitted. - - (* State change vs st_get_tower on different towers *) - - Fact st_get_stack_tower_neq s t l t' : - t <> t' -> (l[t]>s)#t' = s#t'. - Proof. - Admitted. - - (* A sorted state has stricly increasing stacks of disks - over all its three towers *) - - Definition st_sorted (s : state) := - match s with - | (l1,l2,l3) => ↗ l1 /\ ↗ l2 /\ ↗ l3 - end. - - (* Under which condition is a state change sorted ? *) - - Fact st_sorted_stack l t s : - st_sorted (l[t]>s) - <-> st_sorted s /\ l ⪻ s#t /\ ↗ l. - Proof. - Admitted. - - (** A coherent state wrt. a list/multiset of disks - 1) must use each disk exactly once - 2) each tower has to be strictly sorted *) - - Definition st_coh_wrt s ld := st_sorted s /\ ld ~p £s. - - Infix "⋉" := st_coh_wrt (at level 70, no associativity). - - (* The empty state is coherent for the void list of disks *) - - Fact st_empty_coh_wrt_nil : ℰ ⋉ nil. - Proof. - Admitted. - - Hint Resolve st_empty_coh_wrt_nil : core. - - (* Coherence vs change - Hint: use st_stack_tower_collect - *) - - Lemma st_coh_wrt_prefix ld s l t : - s ⋉ ld -> l ⪻ £s -> ↗ l -> l[t]>s ⋉ l++ld. - Proof. - Admitted. - - (* A moves consist in displacing one disk from the top of - one tower to the top of another tower *) - - Inductive move_disk : tower -> disk -> tower -> state -> state -> Prop := - | in_move_disk : forall t x t' s, move_disk t x t' (x::nil[t]>s) (x::nil[t']>s). - - (* move_disk preserves sortedness *) - - Lemma move_disk_sorted s t x t' s' : - move_disk t x t' s s' - -> x::nil ⪻ s#t' - -> st_sorted s - -> st_sorted s'. - Proof. - induction 1 as [ t x t' s ]. - Admitted. - - (* move_disk preserves the multiset of disks *) - - Lemma move_disk_collect s t x t' s' : move_disk t x t' s s' -> £s ~p £s'. - Proof. - Admitted. - - (* move_disk preserves coherence of states *) - - Lemma move_disk_coh ld s t x t' s' : - move_disk t x t' s s' - -> x::nil ⪻ s#t' - -> s ⋉ ld - -> s' ⋉ ld. - Proof. - Admitted. - - (* Valid move is a move - from a coherent state - to another coherent state *) - - Definition move := (tower * tower)%type. - - Definition valid_move_wrt ld s m s' := - s ⋉ ld /\ s' ⋉ ld - /\ match m with - (t,t') => exists x, move_disk t x t' s s' - end. - - Notation "x ~[ m ]~> y ⟦ ld ⟧" := (valid_move_wrt ld x m y). - - (* Valid list of moves *) - - Fixpoint valid_moves_wrt ld s lm s' := - match lm with - | nil => s ⋉ ld /\ s = s' - | m::lm => exists s1, s ~[m]~> s1 ⟦ld⟧ - /\ s1 ~{lm}~> s' ⟦ld⟧ - end - where "x ~{ lm }~> y ⟦ ld ⟧" := (valid_moves_wrt ld x lm y). - - (* A valid list of moves implies coherence wrt. ld *) - - Lemma valid_moves_coh_wrt ld lm s s' : - s ~{lm}~> s' ⟦ld⟧ -> s ⋉ ld /\ s' ⋉ ld. - Proof. - revert s s'; induction lm as [ | m lm IH ]; intros s s'; simpl. - + admit. - + admit. - Admitted. - - (* Valid list of moves and ++ *) - - Lemma valid_moves_wrt_app ld s1 l r s3 : - s1 ~{l++r}~> s3 ⟦ld⟧ - <-> exists s2, s1 ~{l}~> s2 ⟦ld⟧ - /\ s2 ~{r}~> s3 ⟦ld⟧. - Proof. - Admitted. - - (* valid list of moves and _++_::_ *) - - Lemma valid_moves_wrt_hanoi ld s1 l m r s4 : - s1 ~{l++m::r}~> s4 ⟦ld⟧ - <-> exists s2 s3, s1 ~{l}~> s2 ⟦ld⟧ - /\ s2 ~[m]~> s3 ⟦ld⟧ - /\ s3 ~{r}~> s4 ⟦ld⟧. - Proof. - Admitted. - - (* The recursive definition of the Hanoi move of depth n for t <> t' *) - - Fixpoint hanoi_rec n t t' := - match n with - | 0 => nil - | S n => let o := tower_other t t' - in hanoi_rec n t o - ++ (t,t') - :: hanoi_rec n o t' - end. - - Notation ℍr := hanoi_rec. - - (* The exponential function n => 2^n *) - - Fixpoint pow2 n := - match n with - | 0 => 1 - | S n => 2*pow2 n - end. - - (* The length of hanoi_rec is 2^n-1 - Hint: use lia or omega tactic - *) - - Fact hanoi_rec_length n t t' : 1+⌊ℍr n t t'⌋ = pow2 n. - Proof. - Admitted. - - (* Now hanoi whether t = t' or not *) - - Definition hanoi n t t' := - if tower_eq_dec t t' then nil else ℍr n t t'. - - Notation ℍ := hanoi. - - Eval compute in ℍ 3 t1 t2. - - (** Correctness statement for hanoi_rec: - given - - a list of disks ld - - a coherent state s wrt ld - - a sorted stack l - - st. disks in l are smaller than those in s - - two towers t <> t' - then (ℍr ⌊l⌋ t t') is a valid - sequence of moves from l[t]>s to l[t']>s - *) - - (* Hint: a) use reverse list induction - b) this is the longest proof - *) - - Theorem valid_hanoi_rec ld s l t t' : - s ⋉ld - -> ↗ l - -> l ⪻ £s - -> t <> t' - -> l[t]>s ~{ℍr ⌊l⌋ t t'}~> l[t']>s ⟦l++ld⟧. - Proof. - revert ld s t t'. - induction l as [ | l x IHl ] using list_rev_ind. - + admit. - + admit. - Admitted. - - (** If the disks in stack l are strictly smaller than all the disks - stacked in the three tower and l is stricly increasing - then (ℍ (length m) t t') describes a valid sequence - of moves from the state src to state dst where - src := m[t]>s - dst := m[t']>s - - Hint: test whether t =? t' using tower_eq_dec - and then apply valid_hanoi_rec with t <> t' - *) - - Theorem valid_hanoi ld t t' l s : - l ⪻ £s - -> ↗ l - -> s ⋉ ld - -> l[t]>s ~{ℍ ⌊l⌋ t t'}~> l[t']>s ⟦l++ld⟧. - Proof. - Admitted. - - (** If l is a strictly increasing stack then - hanoi ⌊l⌋ t1 t3 is a correct strategy to - displace l stacked on t1 to the same l stacked on t3 *) - - Corollary hanoi_is_correct l : - ↗ l -> l[t1]>ℰ ~{ℍ ⌊l⌋ t1 t3}~> l[t3]>ℰ ⟦l⟧. - Proof. - Admitted. - - Check hanoi_is_correct. - - (** Possible improvements: - (a) show that hanoi is the shortest possible list of moves - (b) show how to sort out any coherent state, not just the - state l[t1]>ℰ so as to put every disk on a given stack *) - -End Hanoi. - - diff --git a/sort.v b/sort.v deleted file mode 100644 index 5aa7691..0000000 --- a/sort.v +++ /dev/null @@ -1,159 +0,0 @@ -(**************************************************************) -(* Copyright Dominique Larchey-Wendling [*] *) -(* *) -(* [*] Affiliation LORIA -- CNRS *) -(**************************************************************) -(* This file is distributed under the terms of the *) -(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *) -(**************************************************************) - -Require Import List Permutation Arith Lia. - -Set Implicit Arguments. - -(** Human friendly notation for lists: - - - x ∈ l : x is a member of l - - l ⊆ m : l is included in m - - ⌊l⌋ : the length of l - - The definitions are to be found in the List - module of the Standart Library - - *) - -Infix "∈" := In (at level 70, no associativity). -Infix "⊆" := incl (at level 70, no associativity). -Notation "⌊ l ⌋" := (length l) (at level 1, format "⌊ l ⌋"). - -Hint Resolve incl_refl incl_appl incl_appr : core. - -(** Strict sorted lists of nat(ural numbers) - - 1) slu (for strictly lower-upper) denoted infix l ⪻ r: - - every member of l is strictly below (<) every member of r - - 2) m is strictly sorted denoted prefix ↗ m: - - for any split m = l++r we have l ⪻ r - -*) - -Definition strict_lower_upper l r := forall x y, x ∈ l -> y ∈ r -> x < y. - -Infix "⪻" := strict_lower_upper (at level 70, no associativity). - -(** A possible definition of strictly increasing list - Exercise: provide alternate characterizations for strictly - increasing lists and show equivalence *) - -Definition si_list m := forall l r, m = l++r -> l ⪻ r. - -Notation "↗ m" := (si_list m) (at level 70). - -Section strict_lists. - - Implicit Type l m : list nat. - - (* ⪻ is decreasing in both arguments - Hint: Check for the definitions of In/∈ and incl/⊆ in the - List module. - *) - - Fact slu_dec l l' m m' : l ⊆ l' -> m ⊆ m' -> l' ⪻ m' -> l ⪻ m. - Proof. - Admitted. - - Fact slu_nil_l l : nil ⪻ l. - Proof. - Admitted. - - Fact slu_nil_r l : l ⪻ nil. - Proof. - Admitted. - - Hint Immediate slu_nil_l slu_nil_r : core. - - (* Equivalences for ⪻ wrt list operators ::, ++ *) - - (* case of singleton lists _::nil *) - - Fact slu_sg_l x l : x::nil ⪻ l <-> forall y, y ∈ l -> x < y. - Proof. - Admitted. - - Fact slu_sg_r x l : l ⪻ x::nil <-> forall y, y ∈ l -> y < x. - Proof. - Admitted. - - (* What about ⪻ and ++ - Hint: in_or_app, in_app_or, in_app_iff *) - - Fact slu_app_l l1 l2 r : l1++l2 ⪻ r <-> l1 ⪻ r /\ l2 ⪻ r. - Proof. - Admitted. - - Fact slu_app_r l r1 r2 : l ⪻ r1++r2 <-> l ⪻ r1 /\ l ⪻ r2. - Proof. - Admitted. - - (* Strictly increasing lists and list operators *) - - Fact si_list_nil : ↗ nil. - Proof. - Admitted. - - Fact si_list_one x : ↗ x::nil. - Proof. - Admitted. - - Hint Resolve si_list_nil si_list_one : core. - - (* Hint: app_ass, in_or_app, in_app_iff and the above app_split *) - - Fact si_list_app l r : ↗ l++r <-> ↗ l /\ ↗ r /\ l ⪻ r. - Proof. - Admitted. - - (* Hint: x::l = (x::nil)++l *) - - Fact si_list_cons x l : ↗ x::l <-> x::nil ⪻ l /\ ↗ l. - Proof. - Admitted. - -End strict_lists. - -Hint Resolve slu_nil_l slu_nil_r - si_list_nil si_list_one : core. - -Section si_list_alt. - - Reserved Notation "'sa' l" (at level 70). - - Inductive si_list_alt : list nat -> Prop := - | in_sa_0 : sa nil - | in_sa_1 : forall x l, (forall y, y ∈ l -> x < y) -> sa l -> sa x::l - where "'sa' l" := (si_list_alt l). - - Fact si_sa l : ↗ l -> sa l. - Admitted. - - Fact sa_si l : sa l -> ↗ l. - Admitted. - - Theorem si_sa_equiv l : ↗l <-> sa l. - Admitted. - -End si_list_alt. - -Check le_lt_dec. - -Lemma bounded_decidable x l : { y | y ∈ l /\ ~ x < y } + { forall y, y ∈ l -> x < y }. -Admitted. - -Lemma slu_decidable l r : { l⪻r } + { ~ l⪻r }. -Admitted. - -Lemma si_decidable l : { ↗l } + { ~ ↗l }. -Admitted. \ No newline at end of file diff --git a/sorting_algorithms.v b/sorting_algorithms.v index 48025f2..185689f 100644 --- a/sorting_algorithms.v +++ b/sorting_algorithms.v @@ -153,8 +153,8 @@ Section perm. End perm. -(** On va trier les listes en utilisant un ordre total décidable, - c'est à dire, une relation binaire +(** On va trier les listes en utilisant un ordre total + et calculable, c'est à dire, une relation binaire R : X -> X -> Prop @@ -177,7 +177,7 @@ Parameter (R_refl : forall x, x ≤ x) (R_cmp : forall x y, { b : bool | if b then x ≤ y else y ≤ x }). (* R_cmp x y est de type { b : bool | if b then x ≤ y else y ≤ x }, càd - une paire dépendante (b,Hb) où + une paire dépendante (b,Hb) où - b est de type bool; - Hb est de type (if b then x ≤ y else y ≤ x). Donc le type de Hb dépend de la valeur de b. Plus précisément, b est true