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-Aug] The end of the Necklaces

Maria has an infinite number of beautiful beads. They come in different colors and she has all the colors there exist.

Her destiny is to craft a new necklace everyday for the queen. Each day the necklace may not be identical to any necklace she did before but also may not take more beads than the queen can bear.

While she is joyfully crafting today's necklace, she suddenly realizes that she won't be able to carry on her life like this forever. Can you prove that she is correct?

[Thanks to the problem author Simon Wimmer, and the translators Sebastian Joosten (ACL2), Kevin Kappelmann (Lean) and Qinshi Wang (Coq).]

Resources

Download Files

Definitions File

theory Defs
imports Main
begin



end

Template File

theory Submission
  imports Defs
begin           

lemma goal: "finite {xs.  length xs ≤ i ∧ set xs ⊆ {0..(n::nat)} }" for i
sorry

end

Check File

theory Check 
  imports Submission
begin




test "finite {xs.  length xs ≤ i ∧ set xs ⊆ {0..(n::nat)} }"  
  by (rule Submission.goal)


end
Download Files

Definitions File

Require Export Coq.Lists.List.
Require Export Coq.Sets.Finite_sets_facts.

Arguments Finite [U] A.
Arguments In [U] A x.

(* Every elements in xs is in A. *)
Definition List_of {U} (A : Ensemble U) xs :=
  Forall (fun x => In A x) xs.

Definition nat_range lo hi : Ensemble nat :=
  (fun x => lo <= x <= hi).

Template File

Require Import Defs.

(* These two axioms are allowed. *)
Check classic.
Check Extensionality_Ensembles.

(* Some useful definitions. *)
Print Ensemble.
Print Finite.
Print cardinal.

(* Useful facts *)
(* Search Finite. *)
(* Search cardinal. *)

Theorem goal : forall n m,
  Finite
    (fun xs => length xs <= m /\ List_of (nat_range 0 n) xs).
Proof.
  (* TODO *)
Admitted.
Download Files

Definitions File

import data.set.finite

Template File

import .defs

lemma marias_destiny (n m : ℕ) : { l : list (fin n) | l.length ≤ m }.finite := sorry

Check File

import .defs
import .submission

lemma poor_maria (n m : ℕ) : { l : list (fin n) | l.length ≤ m }.finite :=
marias_destiny n m
Download Files

Definitions File

(in-package "ACL2")

(defun short-lists (i lst)
  (if (endp lst) (not lst)
    (and (true-listp (car lst))
         (< (len (car lst)) i)
         (short-lists i (cdr lst))
    )
  )
)

Template File

(in-package "ACL2")

(include-book "Defs")

(defun upperbound (i lst)
  (expt (len lst) i) ; this bound is definitely not high enough! Change this definition..
)

(defthm finite-list
  (implies (and (subsetp (flatten necklaces) beads)
                (short-lists max-weight necklaces)
                (no-duplicatesp necklaces)
                (natp max-weight)
                )
           (< (len necklaces)
              (upperbound max-weight beads)))
)

Check File

; The four lines just below are boilerplate, that is, the same for every
; problem.

(in-package "ACL2")
(include-book "Submission")
(set-enforce-redundancy t)
(include-book "Defs")

; The events below represent the theorem to be proved, and are copied from
; template.lisp.

(defthm finite-list
  (implies (and (subsetp (flatten necklaces) beads)
                (short-lists max-weight necklaces)
                (no-duplicatesp necklaces)
                (natp max-weight))
           (< (len necklaces)
              (upperbound max-weight beads)))
)

Terms and Conditions