forked from mvmramos/pumping
-
Notifications
You must be signed in to change notification settings - Fork 0
/
misc_logic.v
36 lines (31 loc) · 1.13 KB
/
misc_logic.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
(* ---------------------------------------------------------------------
This file contains definitions and proof scripts related to
(i) closure operations for context-free grammars,
(ii) context-free grammars simplification
(iii) context-free grammar Chomsky normalization and
(iv) pumping lemma for context-free languages.
More information can be found in the paper "Formalization of the
pumping lemma for context-free languages", submitted to
LATA 2016.
Marcus Vinícius Midena Ramos
--------------------------------------------------------------------- *)
(* --------------------------------------------------------------------- *)
(* BASIC LEMMAS *)
(* --------------------------------------------------------------------- *)
Lemma sig_weak {A: Type} {P P': A -> Prop} (H: forall x: A, P x -> P' x) (a: {x | P x}): {x | P' x}.
Proof.
destruct a as [x H0].
exists x.
apply H.
exact H0.
Qed.
Lemma contrap:
forall P1 P2: Prop,
(P1 -> P2) -> (~ P2 -> ~ P1).
Proof.
intros P1 P2 H1 H2 H3.
apply H2.
apply H1.
exact H3.
Qed.