famubu
/
playground
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

[coq] try some sf1 (lf)

This commit is contained in:
Julin S 2024-01-04 20:53:48 +05:30
parent 25dc1bf9ad
commit 3239f401be
4 changed files with 203 additions and 45 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
coq/list-set/_CoqProject Normal file
View File

@ -0,0 +1,15 @@
-R _build/default/theories aruvi
#_build/default/theories/Nfa.v
#_build/default/theories/FinTyp.v
-I /media/julinusername/eins/gits/math-comp/mathcomp
-R /media/julinusername/eins/gits/math-comp/mathcomp mathcomp
-arg -w -arg -projection-no-head-constant
-arg -w -arg -redundant-canonical-projection
-arg -w -arg -notation-overridden
-arg -w -arg +duplicate-clear
-arg -w -arg +non-primitive-record
-arg -w -arg +undeclared-scope
-arg -w -arg +deprecated-hint-rewrite-without-locality
-arg -w -arg -elpi.add-const-for-axiom-or-sectionvar

178
coq/ltl.v
View File

@ -1,6 +1,7 @@
(* https://www.labri.fr/perso/casteran/CoqArt/chapter13.pdf *)
(* https://github.com/coq-contribs/ltl *)
(* Require Import Streams. *)
(* Lemma unfoldStream {A: Type}: forall s: Stream A, *)
@ -103,24 +104,13 @@ Section streams.
isFinite s -> isFinite (SCons a s).
(* A coinductive predicate. Keeps producing. *)
Inductive isInfinite {A: Type}: stream A -> Prop :=
CoInductive isInfinite {A: Type}: stream A -> Prop :=
| IsInfin: forall (s: stream A) (a:A),
isInfinite s -> isInfinite (SCons a s).
End streams.
Section streamLemmas.
Lemma unfoldStream {A: Type}: forall s: stream A,
s = match s with
| SNil => SNil
| SCons x ss => SCons x ss
end.
Proof.
move => s.
by case: s.
Qed.
End streamLemmas.
Section ltl.
Module Ltl.
Section Foo.
Context {A: Type}.
Definition sProp: Type := stream A -> Prop.
@ -134,59 +124,156 @@ Section ltl.
p s -> next p (SCons a s).
(* Strict eventually *)
Inductive eventually (p: sProp): sProp :=
| FDone: forall (a: A) (s: stream A),
p (SCons a s) -> eventually p (SCons a s)
| FMore: forall (a: A) (s: stream A),
eventually p s -> eventually p (SCons a s).
(* Inductive eventually (p: sProp): sProp := *)
(* | FDone: forall (a: A) (s: stream A), *)
(* p (SCons a s) -> eventually p (SCons a s) *)
(* | FMore: forall (a: A) (s: stream A), *)
(* eventually p s -> eventually p (SCons a s). *)
CoInductive always (p: sProp): sProp :=
| Always: forall (s: stream A) (a: A),
always p s -> always p (SCons a s).
End ltl.
(* CoInductive always (p: sProp): sProp := *)
(* | Always: forall (s: stream A) (a: A), *)
(* always p s -> always p (SCons a s). *)
CoInductive until (p q: sProp): sProp :=
| UDone: forall (s: stream A) (a: A),
q s -> until p q (SCons a s)
| UMore: forall (s: stream A) (a: A),
p s -> until p q s -> until p q (SCons a s).
Definition not (p: sProp): sProp := fun s => not (p s).
Definition or (p q: sProp): sProp := fun s => (p s) \/ (q s).
Definition and (p q: sProp): sProp := or (not p) (not q).
Definition impl (p q: sProp): sProp := or (not p) q.
Definition eventually (p: sProp): sProp := until (fun _ => True) p.
Definition always (p: sProp): sProp := until p (fun _ => False).
End Foo.
End Ltl.
Section streamLemmas.
Context {A: Type}.
Lemma unfoldStream: forall s: stream A,
s = match s with
| SNil => SNil
| SCons x ss => SCons x ss
end.
Proof. by move => s; case: s. Qed.
Lemma sappSNil: forall (s: stream A),
sapp SNil s = s.
Proof.
move => s.
rewrite (unfoldStream (sapp SNil s)).
by case: s.
Qed.
End streamLemmas.
Section Lemmas.
Context (A: Type).
Import Ltl.
Definition satisfies (P: stream A -> Prop) (s: stream A): Prop := P s.
(*
(cofix const (a0 : A) : stream A := SCons a0 (const a0)) a =
SCons a ((cofix const (a0 : A) : stream A := SCons a0 (const a0)) a)
*)
(* rewrite {1}/const. *)
(*
(cofix const (a0 : A) : stream A := SCons a0 (const a0)) a =
SCons a (const a)
*)
Definition XdistributiveOr (p q: sProp): forall s: stream A,
(next (or p q)) s ->
(next p) s \/ (next q) s.
Proof.
move => s H.
elim: H.
move => a s'.
rewrite /or => H.
case: H.
- move => H; left; by apply Next.
- move => H; right; by apply Next.
Qed.
Lemma nextStream: forall (p: sProp) (s: stream A) (a: A),
next p (SCons a s) -> p s.
Proof.
move => p s a H.
case: H.
move => _ s'.
Abort.
Definition XdistributiveU (p q: sProp): forall s: stream A,
(next (until p q)) s ->
(until (next p) (next q)) s.
Proof.
move => s H.
case: s H.
move => H; first by inversion H.
move => a s.
Abort.
(* Definition UdistributiveOr (p q r: sProp): forall s: stream A, *)
(* (until (or p q)) r s -> *)
(* (until p) s \/ (until q) s. *)
(* Proof. *)
(* Definition GdistributiveOr (p q: sProp): forall s: stream A, *)
(* (always (or p q)) s -> *)
(* (always p) s \/ (always q) s. *)
(* Proof. *)
(* rewrite /always. *)
(* move => s H. *)
(* case: H; first by move => s' a. *)
(* move => s' a H. *)
(* rewrite /or. *)
(* move => HH. *)
(* case: HH; first by move => s'' a'. *)
(* split. *)
Theorem nextRepeat: forall (a b: A),
satisfies (next (atom (fun x => x = b))) (SCons a (const b)).
(next (atom (fun x => x = b))) (SCons a (const b)).
Proof.
move => a b.
rewrite /satisfies.
apply Next.
rewrite (unfoldStream (const b)).
rewrite /const.
by apply Atom.
Qed.
Theorem prefixEventually: forall (pre post: stream A) (P: sProp),
Theorem prefixEventually: forall (pre post: stream A) (p: sProp),
isFinite pre ->
satisfies P post ->
satisfies P (sapp pre post).
satisfies (eventually p) post ->
satisfies (eventually p) (sapp pre post).
Proof.
move => pre post P preFin.
move => pre post p HpreFin.
rewrite /satisfies.
case: HpreFin.
- move => H.
case: H.
+ move => a s.
rewrite sappSNil.
apply FDone.
+ move => a s.
rewrite sappSNil.
apply FMore.
- move => s a HsFin.
+ case: HsFin.
*
Abort.
Theorem alwaysInfinite: forall (s: stream A) (P: sProp),
always P s -> isInfinite s.
Theorem alwaysInfinite: forall (s: stream A) (p: sProp),
satisfies (always p) s -> isInfinite s.
Proof.
move => s P H.
move => s p.
rewrite /satisfies.
move => H.
case: H.
rewrite (unfoldStream s).
move => s' a H.
apply IsInfin.
cofix HH.
case: HH.
move => s2 a2 H2.
apply IsInfin.
apply H2.
Fail Qed.
Abort.
End Lemmas.
@ -209,7 +296,7 @@ End Lemmas.
Require Import Streams.
Require Import ssreflect.
Section ltl.
Module Ltl.
Context {A: Type}.
Definition sProp: Type := Stream A -> Prop.
@ -237,10 +324,11 @@ Section ltl.
(* Definition impl (p q: sProp): sProp := ¬p ∨ q. *)
(* Definition eventually (p: sProp): sProp := ⊤ U p. *)
(* Definition always (p: sProp): sProp := p U ⊥. *)
End ltl.
End Ltl.
#[global] Arguments sProp: clear implicits.
Module LtlNotations.
Import Ltl.
Declare Scope ltl_scope.
Delimit Scope ltl_scope with ltl.

12
coq/sf/1-lf-logic.v
View File

@ -192,3 +192,15 @@ Proof.
- induction m.
+ auto.
Abort.
Require Import ssreflect ssrbool.
Theorem eqb_eq: forall (n1 n2: nat),
Nat.eqb n1 n2 = true <-> n1 = n2.
Proof.
move => n1 n2.
case (Nat.eqb n1 n2) eqn:H.
- by rewrite PeanoNat.Nat.eqb_eq in H.
- by rewrite PeanoNat.Nat.eqb_neq in H.
Qed.

43
coq/sf/lf7_IndProp.v Normal file
View File

@ -0,0 +1,43 @@
(* https://softwarefoundations.cis.upenn.edu/lf-current/IndProp.html#lab262 *)
Require Import List.
Import ListNotations.
Require Import ssreflect ssrbool.
Theorem filter_not_empty_In : forall (n: nat) (l: list nat),
(filter (fun x => Nat.eqb n x) l) <> [] ->
In n l.
Proof.
move => n l.
elim: l => [|a l IH]; first by [].
rewrite //=.
destruct (Nat.eqb n a) eqn:H.
- rewrite PeanoNat.Nat.eqb_eq in H => HH.
by left.
- rewrite PeanoNat.Nat.eqb_neq in H => HH.
by right; apply IH.
Qed.
Print Bool.reflect.
(*
Inductive reflect (P : Prop) : bool -> Set :=
ReflectT : P -> reflect P true | ReflectF : ~ P -> reflect P false.
*)
Theorem iff_reflect: forall (P: Prop) (b: bool),
(P <-> b = true) -> reflect P b.
Proof.
move => P b.
case b => H.
- by apply ReflectT; rewrite H.
- by apply ReflectF; rewrite H.
Qed.
Theorem reflect_iff: forall (P: Prop) (b: bool),
reflect P b -> (P <-> b = true).
Proof.
move => P b.
case b => H.
- case H.
+ rewrite HH.