Preuves sur les chaînes en coq

Question

Je souhaite prouver la propriété 'reflexivity' sur les chaînes. S'il vous plaît, si vous pouvez m'aider comment procéder avec la preuve. Voici mon code:

Fixpoint beq_str (sa sb : String.string) {struct sb}: bool := 
    match sa, sb with 
| EmptyString, EmptyString => true 
| EmptyString, String b sb' => false 
| String a sa', EmptyString => false 
| String a sa', String b sb'=> match (ascii_dec a b) with 
           | left _ => beq_str sa' sb' 
           | right _ => false 
           end 
end. 
(* compares two string names [n1] and [n2] of type [id'] - returs bool. *) 
Definition beq_names n1 n2 := 
    match (n1, n2) with 
    (name s1, name s2) => beq_str s1 s2 
    end. 

Theorem reflexivty : forall i, 
    true = beq_str i i. 
Proof. 
    intros. induction i. 
    auto. simpl. Admitted. 

Answer 1

Je ne sais pas si les devoirs ou des études indépendantes ...

Theorem beq_str_refl : forall i, 
    true = beq_str i i. 
Proof. 
    induction 0; simpl; try (rewrite <- IHi; case (ascii_dec a a)); 
    try reflexivity; intro C; elimtype False; apply C; reflexivity. 
Qed. 

Cela devrait fonctionner.

S'il s'agit de devoirs et que vous êtes paresseux, votre tuteur refusera, espérons-le. Si vous voulez le comprendre et le prouver vous-même, les blocs de construction dont vous avez besoin sont là, il suffit de le démonter et de lancer des pièces à l'état de preuve actuel.

Il y a deux choses icky dans cette preuve. Le premier est de se débarrasser du (ascii_dec a a). (l'analyse de cas sur a ne fonctionnera pas.) Faites l'analyse de cas sur le tout (c'est-à-dire (ascii_dec a a)) pour obtenir deux sous-objectifs, l'un avec l'hypothèse ajoutée a = a, l'autre avec a <> a.

Le deuxième problème peut être de travailler avec des contradictions, sauf si vous avez déjà fait cela.

a <> a est équivalent à a = a -> False. a = a est vrai par définition, ce qui permet de construire une valeur de type False (une contradiction - False n'a pas de constructeurs). Cela vous permet de simplement jeter votre objectif actuel (true = false est impossible à prouver de toute façon), et juste construire cette valeur impossible False.

elimtype False Pour indiquer à Coq que vous souhaitez procéder par analyse de cas sur False. Comme False n'a pas de constructeur, cela vous laisse avec un seul but de construire une valeur de False. Normalement, ce serait impossible, mais vous avez une contradiction entre vos hypothèses. apply cette contradiction (nommé C dans mon script de preuve ci-dessus) et tout ce que vous avez à faire est d'afficher a = a, qui résulte de reflexivity.

---

Voici une version plus lisible que vous pouvez parcourir:

Theorem beq_str_refl : forall i, true = beq_str i i. 
    intro i. induction i as [ | a i IHi ]. 
    (* base case: Empty String *) reflexivity. 
    (* inductive case: *) simpl. rewrite <- IHi. 
     (* do case analysis on ascii_dec (or {a=a}+{a<>a}) *) 
     destruct (ascii_dec a a) as [ Heq | C ]. 
     (* {a = a} *) reflexivity. 
     (* {a <> a} *) unfold not in C. elimtype False. apply C. reflexivity. 

Une autre façon de gérer les contradictions:

(* just a quick nonsensical goal *) 
Theorem foo: forall i, i <> i -> 2 + 2 = 5. 
    intros i C. 
    (* explicitly construct a 'False' value *) 
    assert False as H. 
    apply C. reflexivity. 
    (* 'inversion' generates one goal per possible constructor *) 
    (* as False has no constructors, this gives 0 subgoals, finishing the proof *) 
    inversion H. 
Qed.