Jonathan Certes

Home / Resources / Examples of simple theorems based on LTL_Coq library

Introduction

Coq is an interactive theorem prover. It allows for expressing mathematical assertions, mechanically checks proofs of these assertions, helps find formal proofs, and extracts a certified program from the constructive proof of its formal specification. Coq is not an automated theorem prover but includes automatic theorem proving tactics (procedures) and various decision procedures.

LTL_Coq is a library developed by Cenobio Moisés Vázquez Reyes and available here . It contains a simple formalization of many LTL concepts and theorems. This includes definitions of formulas, paths and LTL semantics. LTL (Linear Temporal Logic) is a modal temporal logic with modalities referring to time.

Examples

Coq provides many mechanics to prove a theorem. Here we only show a subset as a reminder.

Apply tactics on all branches of an induction

Use parentheses. This might remove some branches of the induction in case the tactics are sufficient.

Lemma negP_invol :
  forall p : PathF,
    negP (negP p) = p.
Proof.
  intros p.

  induction p;
  (* we apply these two tactics on each branch of the induction: *)
  (simpl; intuition).
  (* this application removes the two first branches. Then: *)
  - rewrite IHp1.
    rewrite IHp2.
    reflexivity.
  - rewrite IHp1; rewrite IHp2; reflexivity.
  - rewrite IHp1; rewrite IHp2; reflexivity.
  - rewrite IHp1; rewrite IHp2; reflexivity.
  - rewrite IHp; reflexivity.
Qed.

Rewrite or apply a lemme to an hypothesis or a goal

Use the rewritetactic or the apply tactic. Rewriting is only possible in case of equality. Application requires to prove the hypothesis of the lemme.

Lemma negP_forms_state:
  forall π: Path,
    forall s: State,
      forall p: PathF,
        ( (path_up π s ⊨ p) -> ~(path_up π s ⊨ negP p) ).
Proof.
  intros π; intros s; intros p.
  intros H1.
  unfold not.
  intros H2.
  apply   negP_forms in H2.
  rewrite negP_invol in H2.
  unfold not in H2.
  apply H2 in H1.
  case H1.
Qed.

Destruct temporal operators and manipulate states

Using LTL_Coq library, we can make an hypothesis about existing states and manipulate them in other hypothesis and goals.

Variable (π: Path).
Variable (a b: PathF).

Hypothesis ф₁: π ⊨ F(a).
Hypothesis ф₂: π ⊨ G(a --> F(b)).

Theorem ф: π ⊨ F(a ∧ F(b)).
Proof.
  simpl in ф₁.
  simpl.

  (* according to ф₁, I know there exists a State where "a" is top, so I pose
     "s: State" and I remove ∃i from ф₁: *)
  destruct ф₁ as (s & H).
  (* I think that "i0", state in ф where "a" is top, is my hypothesis "s"; so I
     instantiate ∃i0 = s: *)
  exists s.

  split.    (* F() in ф: "a" is top at one state AND bot at all states before *)

  (* state where "a" is top *)
  - split.  (* proving "a" and "F(b)" in F() in ф *)
    * destruct H as (H1 & H2); exact H1.  (* "F(a)" is in ф₁ *)
    * simpl in ф₂.               (* we need ф₂ to prove "F(b)" *)
      destruct ф₂ as [H1 | H2].  (* F() in ф₂, "b" is top at one state AND bot
                                    all states before *)
      + pose (H2 := H1 s).        (* get to state "s", where "a" is top in ф₁ *)
        destruct H2 as [H2 | H3]. (* globally either "¬a" or "F(b)" *)
        (* case of "¬a" in ф₂: "a" cannot be both top in ф₁ and bot here *)
        --  destruct H as (H3 & H4).
            apply negP_forms_state in H3.
            apply H3 in H2.
            case H2.
        (* case of "F(b)" in ф₂ *)
        -- exact H3.
      (* every state before having "b" in ф₂, an hypothesis is false *)
      + destruct H2 as (H2 & H3).
        destruct H3 as (H3 & H4).
        apply state_top in H3.
        case H3.
  (* every state before having "a", I have bot *)
  - intros.
    apply state_bot.
Qed.

Makefile

Compilation of a Coq program is conducted by coqc. We must compile both the library and our program for the proof to work.

Here is a Makefile that provides the recipe (make sure to indent with tabulations):

PROOF = proof.v
DEPS  = LTL.v

BASENAME = $(basename ${PROOF})
DEPSNAME = $(basename ${DEPS})

all: ${PROOF} $(addsuffix .vos, ${DEPSNAME})
    coqc -verbose ${PROOF}
    @echo "The proof has run correctly."

%.vos : %.v
    coqc -verbose $^

clean:
    $(RM) $(addsuffix .glob, ${DEPSNAME}) $(addsuffix .vo  , ${DEPSNAME})
    $(RM) $(addsuffix .vok , ${DEPSNAME}) $(addsuffix .vos , ${DEPSNAME})
    $(RM) $(addsuffix .aux , $(addprefix ., ${DEPSNAME}))
    $(RM) $(addsuffix .glob, ${BASENAME}) $(addsuffix .vo  , ${BASENAME})
    $(RM) $(addsuffix .vok , ${BASENAME}) $(addsuffix .vos , ${BASENAME})
    $(RM) $(addsuffix .aux , $(addprefix ., ${BASENAME}))

Associated resources

Here is an archive which contains the discussed example and its Makefile. Library LTL_Coq is not distributed here, please refer to its repository to download it.

---