CODEWITHSUNDEEP
stringcoq
Khan
Khan

Reputation: 303

Proofs on strings in coq

I want to prove 'reflexivity' property on strings. Please if you can help me how to proceed with the proof. Here is my 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.

Upvotes: 0

Views: 611

Answers (1)

nobody
nobody

Reputation: 4264

Not sure if homework or independent studies...

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.

This should work.

If this is homework and you're lazy, your tutor will hopefully reject this. If you want to understand and prove it yourself, the building blocks you need are in there, just take it apart and throw pieces at your current proof state.

There are two icky things in this proof. First one is getting rid of the (ascii_dec a a). (case-analysis on a won't work.) Do case-analysis on the whole thing (i.e. (ascii_dec a a)) to get two subgoals, one with the added hypothesis a = a, the other with a <> a.

The second problem may be working with contradictions, unless you've done that before.

a <> a is equivalent to a = a -> False. a = a is true by definition, which allows constructing a value of type False (a contradiction -- False has no constructors). This allows you to just throw away your current goal (true = false is impossible to prove anyway), and just construct that impossible False value.

Do elimtype False to tell Coq that you want to proceed by case-analysis on False. As False has no constructors, this leaves you with a single goal of constructing a value of False. Normally that would be impossible, but you've got a contradiction among your hypotheses. apply this contradiction (named C in my proof script above) and all you've left to do is show a = a, which follows from reflexivity.

Here is a more readable version that you can step through:

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.

Another way to handle 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.

Upvotes: 1

Related Questions