mirror of
https://github.com/KevinMidboe/linguist.git
synced 2025-10-29 17:50:22 +00:00
7363241531
New Verilog examples and Coq examples for additional training have been added since linguist is currently failing Coq/Verilog recognition tasks (see #201). In case it wasn't obvious, linguist will not currently pass these new, added test cases.
313 lines
5.5 KiB
Coq
Executable File
313 lines
5.5 KiB
Coq
Executable File
Require Export Logic.
|
|
Import Playground1.
|
|
|
|
Definition relation (X:Type) := X -> X -> Prop.
|
|
|
|
Definition partial_function {X:Type} (R: relation X) :=
|
|
forall x y1 y2 : X, R x y1 -> R x y2 -> y1 = y2.
|
|
|
|
Theorem next_nat_partial_function :
|
|
partial_function next_nat.
|
|
Proof.
|
|
unfold partial_function.
|
|
intros x y1 y2 P Q.
|
|
inversion P.
|
|
inversion Q.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Theorem le_not_a_partial_function :
|
|
~ (partial_function le).
|
|
Proof.
|
|
unfold not.
|
|
unfold partial_function.
|
|
intros H.
|
|
assert (O = S O) as Nonsense.
|
|
Case "Proof of assertion.".
|
|
apply H with O.
|
|
apply le_n.
|
|
|
|
apply le_S.
|
|
apply le_n.
|
|
|
|
inversion Nonsense.
|
|
Qed.
|
|
|
|
Theorem total_relation_not_partial_function :
|
|
~ (partial_function total_relation).
|
|
Proof.
|
|
unfold not.
|
|
unfold partial_function.
|
|
intros H.
|
|
assert (O = S O) as Nonsense.
|
|
apply H with O.
|
|
apply total_relation1.
|
|
|
|
apply total_relation1.
|
|
|
|
inversion Nonsense.
|
|
Qed.
|
|
|
|
Theorem empty_relation_not_partial_funcion :
|
|
partial_function empty_relation.
|
|
Proof.
|
|
unfold partial_function.
|
|
intros x y1 y2.
|
|
intros H.
|
|
inversion H.
|
|
Qed.
|
|
|
|
Definition reflexive {X:Type} (R: relation X) :=
|
|
forall a : X, R a a.
|
|
|
|
Theorem le_reflexive :
|
|
reflexive le.
|
|
Proof.
|
|
unfold reflexive.
|
|
intros n. apply le_n.
|
|
Qed.
|
|
|
|
Definition transitive {X:Type} (R: relation X) :=
|
|
forall a b c : X, (R a b) -> (R b c) -> (R a c).
|
|
|
|
Theorem le_trans:
|
|
transitive le.
|
|
Proof.
|
|
intros n m o Hnm Hmo.
|
|
induction Hmo.
|
|
Case "le_n". apply Hnm.
|
|
Case "le_S". apply le_S. apply IHHmo.
|
|
Qed.
|
|
|
|
Theorem lt_trans:
|
|
transitive lt.
|
|
Proof.
|
|
unfold lt. unfold transitive.
|
|
intros n m o Hnm Hmo.
|
|
apply le_S in Hnm.
|
|
apply le_trans with (a := (S n)) (b := (S m)) (c := o).
|
|
apply Hnm.
|
|
apply Hmo.
|
|
Qed.
|
|
|
|
Theorem lt_trans' :
|
|
transitive lt.
|
|
Proof.
|
|
unfold lt. unfold transitive.
|
|
intros n m o Hnm Hmo.
|
|
induction Hmo as [| m' Hm'o].
|
|
apply le_S.
|
|
apply Hnm.
|
|
|
|
apply le_S.
|
|
apply IHHm'o.
|
|
Qed.
|
|
|
|
Theorem le_Sn_le: forall n m, S n <= m -> n <= m.
|
|
Proof.
|
|
intros n m H. apply le_trans with (S n).
|
|
apply le_S. apply le_n.
|
|
apply H. Qed.
|
|
|
|
Theorem le_S_n : forall n m,
|
|
(S n <= S m) -> (n <= m).
|
|
Proof.
|
|
intros n m H.
|
|
apply Sn_le_Sm__n_le_m.
|
|
apply H.
|
|
Qed.
|
|
|
|
Theorem le_Sn_n : forall n,
|
|
~ (S n <= n).
|
|
Proof.
|
|
induction n.
|
|
intros H.
|
|
inversion H.
|
|
|
|
unfold not in IHn.
|
|
intros H.
|
|
apply le_S_n in H.
|
|
apply IHn.
|
|
apply H.
|
|
Qed.
|
|
|
|
(*
|
|
TODO
|
|
Theorem lt_trans'' :
|
|
transitive lt.
|
|
Proof.
|
|
unfold lt. unfold transitive.
|
|
intros n m o Hnm Hmo.
|
|
induction o as [| o'].
|
|
*)
|
|
|
|
Definition symmetric {X: Type} (R: relation X) :=
|
|
forall a b : X, (R a b) -> (R b a).
|
|
|
|
Definition antisymmetric {X : Type} (R: relation X) :=
|
|
forall a b : X, (R a b) -> (R b a) -> a = b.
|
|
|
|
Theorem le_antisymmetric :
|
|
antisymmetric le.
|
|
Proof.
|
|
intros a b.
|
|
generalize dependent a.
|
|
induction b.
|
|
intros a.
|
|
intros H.
|
|
intros H1.
|
|
inversion H.
|
|
reflexivity.
|
|
|
|
intros a H1 H2.
|
|
destruct a.
|
|
inversion H2.
|
|
|
|
apply Sn_le_Sm__n_le_m in H1.
|
|
apply Sn_le_Sm__n_le_m in H2.
|
|
apply IHb in H1.
|
|
rewrite H1 in |- *.
|
|
reflexivity.
|
|
|
|
apply H2.
|
|
Qed.
|
|
|
|
(*
|
|
TODO
|
|
Theorem le_step : forall n m p,
|
|
n < m ->
|
|
n <= S p ->
|
|
n <= p.
|
|
Proof.
|
|
*)
|
|
|
|
Definition equivalence {X:Type} (R: relation X) :=
|
|
(reflexive R) /\ (symmetric R) /\ (transitive R).
|
|
|
|
Definition order {X:Type} (R: relation X) :=
|
|
(reflexive R) /\ (antisymmetric R) /\ (transitive R).
|
|
|
|
Definition preorder {X:Type} (R: relation X) :=
|
|
(reflexive R) /\ (transitive R).
|
|
|
|
Theorem le_order :
|
|
order le.
|
|
Proof.
|
|
unfold order. split.
|
|
Case "refl". apply le_reflexive.
|
|
split.
|
|
Case "antisym". apply le_antisymmetric.
|
|
Case "transitive". apply le_trans. Qed.
|
|
|
|
Inductive clos_refl_trans {A:Type} (R: relation A) : relation A :=
|
|
| rt_step : forall x y, R x y -> clos_refl_trans R x y
|
|
| rt_refl : forall x, clos_refl_trans R x x
|
|
| rt_trans : forall x y z,
|
|
clos_refl_trans R x y -> clos_refl_trans R y z -> clos_refl_trans R x z.
|
|
|
|
Theorem next_nat_closure_is_le : forall n m,
|
|
(n <= m) <-> ((clos_refl_trans next_nat) n m).
|
|
Proof.
|
|
intros n m.
|
|
split.
|
|
intro H.
|
|
induction H.
|
|
apply rt_refl.
|
|
|
|
apply rt_trans with m.
|
|
apply IHle.
|
|
|
|
apply rt_step.
|
|
apply nn.
|
|
|
|
intro H.
|
|
induction H.
|
|
inversion H.
|
|
apply le_S.
|
|
apply le_n.
|
|
|
|
apply le_n.
|
|
|
|
apply le_trans with y.
|
|
apply IHclos_refl_trans1.
|
|
|
|
apply IHclos_refl_trans2.
|
|
Qed.
|
|
|
|
Inductive refl_step_closure {X : Type} (R: relation X)
|
|
: X -> X -> Prop :=
|
|
| rsc_refl : forall (x : X), refl_step_closure R x x
|
|
| rsc_step : forall (x y z : X), R x y ->
|
|
refl_step_closure R y z ->
|
|
refl_step_closure R x z.
|
|
|
|
Tactic Notation "rt_cases" tactic(first) ident(c) :=
|
|
first;
|
|
[ Case_aux c "rt_step" | Case_aux c "rt_refl" | Case_aux c "rt_trans" ].
|
|
|
|
Tactic Notation "rsc_cases" tactic(first) ident(c) :=
|
|
first;
|
|
[ Case_aux c "rsc_refl" | Case_aux c "rsc_step" ].
|
|
|
|
Theorem rsc_R : forall (X:Type) (R:relation X) (x y:X),
|
|
R x y -> refl_step_closure R x y.
|
|
Proof.
|
|
intros X R x y r.
|
|
apply rsc_step with y.
|
|
apply r.
|
|
|
|
apply rsc_refl.
|
|
Qed.
|
|
|
|
Theorem rsc_trans :
|
|
forall (X : Type) (R : relation X) (x y z : X),
|
|
refl_step_closure R x y ->
|
|
refl_step_closure R y z ->
|
|
refl_step_closure R x z.
|
|
Proof.
|
|
intros X.
|
|
intros R x y z.
|
|
intros H.
|
|
induction H.
|
|
intros H1.
|
|
apply H1.
|
|
|
|
intros H1.
|
|
apply IHrefl_step_closure in H1.
|
|
apply rsc_step with y.
|
|
apply H.
|
|
|
|
apply H1.
|
|
Qed.
|
|
|
|
Theorem rtc_rsc_coincide:
|
|
forall (X:Type) (R: relation X) (x y : X),
|
|
clos_refl_trans R x y <-> refl_step_closure R x y.
|
|
Proof.
|
|
intros X R x y.
|
|
split.
|
|
intros H.
|
|
induction H.
|
|
apply rsc_step with y.
|
|
apply H.
|
|
|
|
apply rsc_refl.
|
|
|
|
apply rsc_refl.
|
|
|
|
apply rsc_trans with y.
|
|
apply IHclos_refl_trans1.
|
|
|
|
apply IHclos_refl_trans2.
|
|
|
|
intros H1.
|
|
induction H1.
|
|
apply rt_refl.
|
|
|
|
apply rt_trans with y.
|
|
apply rt_step.
|
|
apply H.
|
|
|
|
apply IHrefl_step_closure.
|
|
Qed.
|