Library Intro

In this section we introduce the very basic definitions necessary for our development. There is nothing here that is tied with the concepts of the Fractal Component Model.

It can be seen however, a gentle and very brief introduction to the Coq Proof Assistant. Therefore, it can be of great benefit for those wanting to know more about this overall Coq development without having a previous background in Coq or even interactive theorem proving.

On the other hand, the reader acquainted with The Coq Proof Assistant may want to skip this section.

Basic Definitions

Require Export Coq.Lists.List. Require Export Coq.Strings.String.
Require Export Coq.Strings.Ascii.
Require Export Coq.Bool.Bool.
Load Batteries.

Inductive ident : Type :=
  | Ident : string -> ident.

Module IdentDefinitionExample.

Definition FooVariable : ident := Ident "foo".
Definition BarVariable : ident := Ident "bar".
Definition XyzVariable : ident := Ident "foo".

End IdentDefinitionExample.

Function beq_ident (id1 id2: ident) : bool :=
  match id1, id2 with
    | Ident str1, Ident str2 => match string_dec str1 str2 with

                                      | left _ => true
                                      | right _ => false
                                   end
  end.

Notation "s1 '==' s2" := (beq_ident s1 s2) (at level 80).

Lemma ident_dec : forall id1 id2 : ident, {id1 = id2} + {id1 <> id2}.
Proof.
  repeat decide equality.
Qed.

Axiom ident_refl : forall id , (id == id ) = true.

Axiom str_symmetry :
  forall str1 str2, (if string_dec str1 str2 then true else false ) =
                              (if string_dec str2 str1 then true else false ).

Lemma beq_ident_symmetry:
  forall i i' X, (i == i') = X <-> (i' == i) = X.
Proof.
  intros.
  destruct X.
  Case "Evals to True".
    split.
    SCase "Left entails right".
      intro. functional induction beq_ident i i'.
      SSCase "Idents are equal".
        unfold beq_ident.
        rewrite e1; auto.
      SSCase "Idents are not equal".
        thus congruence.
    SCase "Right entails left".
      intro. functional induction beq_ident i' i.
      SSCase "Idents are equal".
        unfold beq_ident.
        rewrite e1; auto.
    SSCase "Idents are not equal".
      thus congruence.
   Case "Evals to False".
    split.
    SCase "Left entails right".
      intro. functional induction beq_ident i i'.
      SSCase "Idents are equal".
        unfold beq_ident.
        rewrite e1; auto.
      SSCase "Idents are not equal".
        unfold beq_ident.
        rewrite str_symmetry.
        rewrite e1.
        auto.
    SCase "Right entails left".
      intro. functional induction beq_ident i' i.
      SSCase "Idents are equal".
        unfold beq_ident.
        rewrite e1; auto.
    SSCase "Idents are not equal".
      unfold beq_ident.
      rewrite str_symmetry.
      rewrite e1.
      auto.
Qed.

Lemma bool_conjunction_fact:
  forall id id' X,
    (id == id') && X = true ->
    (id == id') = true.
Proof.
  intros.
  functional induction beq_ident id id'; auto.
Qed.

Hint Resolve bool_conjunction_fact.

Lemma bool_conjunction_fact':
  forall id id' X,
    X && (id == id') = true ->
    (id == id') = true.
Proof.
  intros.
  assert (X && (id == id') = (id == id') && X).
    intuition.
  rewrite H0 in H.
  functional induction beq_ident id id'; auto.
Qed.

Hint Resolve bool_conjunction_fact'.

Lemma ident_equality_Prop2bool:
   forall id id',
   id = id' ->
   (id == id') = true.
Proof.
  intros.
  functional induction beq_ident id id'; auto.
  congruence.
Qed.

Lemma ident_equality_Prop2bool':
   forall id id',
   id <> id' ->
   (id == id') = false.
Proof.
  intros.
  functional induction beq_ident id id'; auto.
  congruence.
Qed.

Lemma ident_equality_bool2Prop:
   forall id id',
   (id == id') = false -> id <> id'.
Proof.
  intros.
  functional induction beq_ident id id'.
  congruence.
  intuition.
  apply _x; auto.
  inversion H0; auto.
Qed.

Lemma ident_equality_bool2Prop':
   forall id id',
   (id == id') = true -> id = id'.
Proof.
  intros.
  functional induction beq_ident id id'; auto.
  congruence.
Qed.

Hint Resolve ident_equality_Prop2bool ident_equality_Prop2bool'
             ident_equality_bool2Prop ident_equality_bool2Prop'.

Lemma beq_ident_symmetry':
  forall i i', (i == i') = false <-> (i' == i) = false.
Proof.
  intros.
  destruct ident_dec with (id1:=i) (id2:=i').
  Case "Ids are equal".
    assert ((i == i') = true).
      eauto.
    subst.
    rewrite H.
    split; congruence.
  Case "Ids are not Equal".
    assert ((i == i') = false).
      eauto.
    assert ((i' == i) = false).
      eauto.
    rewrite H; rewrite H0; intuition.
Qed.

Hint Resolve beq_ident_symmetry'.

Definition bneq_ident id1 id2 : bool :=
match beq_ident id1 id2 with
   | true => false
   | false => true
end.

Notation "s1 '!=' s2" := (bneq_ident s1 s2) (at level 80).

Bind Scope id_scope with ident.
Delimit Scope id_scope with id.

Warming up: Some Simple Proof Examples

So far, we just defined the notion of identifiers, let's see what can we prove about them.

Module IdentProofExamples.

Definition x : ident := Ident "x".
Definition y : ident := Ident "y".

Example warm_up_proof :
   x = y -> False.
Proof.
   intro.
   thus inversion H.
Qed.

Example warm_up_proof':
   (x == y ) = false.
Proof.
   unfold beq_ident.
   thus auto.
Qed.

End IdentProofExamples.

Definition ErrorIdent : ident := Ident "ExceptionIdent".

Require Export Arith.EqNat.

Hint Resolve ident_dec beq_ident_symmetry.