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.

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).]

Download Files
### Definitions File

### Template File

### Check File

theory Defs imports Main begin end

theory Submission imports Defs begin lemma goal: "finite {xs. length xs ≤ i ∧ set xs ⊆ {0..(n::nat)} }" for i sorry end

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

### Template 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).

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

### Template File

### Check File

import data.set.finite

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

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

### Template File

### Check 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)) ) ) )

(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))) )

; 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