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.

# 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

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

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

end
```

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

### 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```

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

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

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

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

end
```

Terms and Conditions