Définition de la fonction récursive en coq avec limite sur l'ensemble des entrées possibles

Question

Je dois définir une fonction récursive sans argument facilement mesurable. Je garde une liste d'arguments utilisés pour m'assurer que chacun est utilisé au maximum une fois, et l'espace d'entrée est fini. Utiliser une mesure (inpspacesize - (length l)) fonctionne principalement, mais je suis coincé dans un cas. Il semble que je manque l'information que les couches précédentes de l ont été construites correctement, je. e. il n'y a pas de doublons et toutes les entrées proviennent vraiment de l'espace d'entrée.

Maintenant, je cherche un remplacement de liste qui fait ce dont j'ai besoin.

Modifier J'ai réduit ce qui suit maintenant:

Je nat s plus petit qu'un donné max et la nécessité de faire en sorte que la fonction est appelée au plus une fois pour chaque numéro. Je suis venu avec ce qui suit:

(* the condition imposed *) 
Inductive limited_unique_list (max : nat) : list nat -> Prop := 
    | LUNil : limited_unique_list max nil 
    | LUCons : forall x xs, limited_unique_list max xs 
      -> x <= max 
      -> ~ (In x xs) 
      -> limited_unique_list max (x :: xs). 

(* same as function *) 
Fixpoint is_lulist (max : nat) (xs0 : list nat) : bool := 
    match xs0 with 
    | nil  => true 
    | (x::xs) => if (existsb (beq_nat x) xs) || negb (leb x max) 
       then false 
       else is_lulist max xs 
    end. 

(* really equivalent *) 
Theorem is_lulist_iff_limited_unique_list : forall (max:nat) (xs0 : list nat), 
    true = is_lulist max xs0 <-> limited_unique_list max xs0. 
Proof. ... Qed. 

(* used in the recursive function's step *) 
Definition lucons {max : nat} (x : nat) (xs : list nat) : option (list nat) := 
    if is_lulist max (x::xs) 
    then Some (x :: xs) 
    else None. 

(* equivalent to constructor *) 
Theorem lucons_iff_LUCons : forall max x xs, limited_unique_list max xs -> 
    (@lucons max x xs = Some (x :: xs) <-> limited_unique_list max (x::xs)). 
Proof. ... Qed. 

(* unfolding one step *) 
Theorem lucons_step : forall max x xs v, @lucons max x xs = v -> 
    (v = Some (x :: xs) /\ x <= max /\ ~ (In x xs)) \/ (v = None). 
Proof. ... Qed. 

(* upper limit *) 
Theorem lucons_toobig : forall max x xs, max < x 
    -> ~ limited_unique_list max (x::xs). 
Proof. ... Qed. 

(* for induction: increasing max is ok *) 
Theorem limited_unique_list_increasemax : forall max xs, 
    limited_unique_list max xs -> limited_unique_list (S max) xs. 
Proof. ... Qed. 

je continue à me coincer en essayant de prouver que je peux inductivement insérer un élément dans la liste complète (soit l'IH sort inutilisable ou je ne peux pas trouver les informations J'ai besoin). Comme je pense que cette non-insertion est cruciale pour montrer la fin, je n'ai toujours pas trouvé de solution de travail.

Des suggestions sur la façon de prouver cela différemment, ou sur la restructuration de ce qui précède?

Answer 1

Difficile à dire beaucoup sans plus de détails (s'il vous plaît préciser!), Mais:

• Utilisez-vous la commande Program? C'est certainement très utile pour définir des fonctions avec des mesures non triviales.
• Pour l'unicité ne fonctionnerait-il pas si vous avez essayé des ensembles? Je me souviens avoir écrit une fonction qui ressemble beaucoup à ce que vous dites: j'avais une fonction pour laquelle un argument contenait un ensemble d'éléments. Cet ensemble d'objets se développait de façon monotone et se limitait à un espace fini d'éléments, donnant l'argument de terminaison.