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).]
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
lemma "finite {xs. length xs ≤ i ∧ set xs ⊆ {0..(n::nat)} }"
by (rule Submission.goal)
end
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.
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
(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)))
)
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
lemma "finite {xs. length xs ≤ i ∧ set xs ⊆ {0..(n::nat)} }"
by (rule Submission.goal)
end