311 lines
20 KiB
Coq
Executable File
311 lines
20 KiB
Coq
Executable File
(* extensions- (hopefully) the final version of worlds_prim/entails_def *)
|
|
|
|
Load CDS_prims.
|
|
|
|
Module entails_def.
|
|
Definition p_entails := fun p q : prop => forall w : world, (p@w) = true -> (q@w) = true.
|
|
End entails_def.
|
|
|
|
Module Import Ultra := Ult entails_def.
|
|
|
|
Section prop_axioms.
|
|
Axiom p_and_ax : forall (p q : prop) (w : world), ((p and q)@w) = ((p@w) && (q@w)).
|
|
Axiom p_or_ax : forall (p q : prop) (w : world), ((p or q)@w) = ((p@w) || (q@w)).
|
|
Axiom p_implies_ax : forall (p q : prop) (w : world), ((p implies q)@w) = ((p@w) ~> (q@w)).
|
|
Axiom p_iff_ax : forall (p q : prop) (w : world), ((p iff q)@w) = (((p implies q)@w) && ((q implies p)@w)).
|
|
Axiom p_not_ax : forall (p : prop) (w : world), ((not p)@w) = -~(p@w).
|
|
Axiom truth_ax : forall w : world, (truth@w) = true.
|
|
Axiom falsity_ax : forall w : world, (falsity@w) = false.
|
|
Axiom p_equals_ax : forall (s : statterm) (x y : (Sns s)) (w : world), (((p_equals s x y)@w) = true) <-> (x = y).
|
|
Axiom p_exists_ax : forall (s : statterm) (R : (Sns s) -> prop) (w : world),
|
|
(((p_exists s R)@w) = true) <-> ~(forall x : (Sns s), ((R x)@w) = false).
|
|
Axiom p_forall_ax : forall (s : statterm) (R : (Sns s) -> prop) (w : world),
|
|
(((p_forall s R)@w) = true) <-> (forall x : (Sns s), ((R x)@w) = true).
|
|
End prop_axioms.
|
|
|
|
Section Useful_lemmas.
|
|
Definition eq_trans' : forall {A : Type} {x y z : A}, x = y -> x = z -> y = z
|
|
:= fun (A : Type) (x y z : A) (u : x = y) (v : x = z) => match u in (_ = a) return (a = z) with eq_refl => v end.
|
|
|
|
Definition tnf : true <> false := eq_ind true (fun b : bool => if b then True else False) I false.
|
|
End Useful_lemmas.
|
|
|
|
Section prop_Theorems.
|
|
Definition facts_ultra : forall w : world, ultrafilter (facts w)
|
|
:= fun w : world =>
|
|
conj (fun (p q : prop) (e : (p@w) = true) (f : p entails q) => f w e)
|
|
(conj (fun (p q : prop) (u : (p@w) = true) (v : (q@w) = true) => eq_trans (p_and_ax p q w) (f_equal2 andb u v))
|
|
(conj (fun p : prop => (if (p@w) as b return ((p@w) = b -> ((p@w) = true) \/ (((not p)@w) = true))
|
|
then (fun u : (p@w) = true => or_introl u)
|
|
else (fun v : (p@w) = false => or_intror (eq_trans (p_not_ax p w) (f_equal negb v))))
|
|
eq_refl)
|
|
(falsity_ax w))).
|
|
|
|
Definition entail_refl : forall p : prop, p entails p
|
|
:= fun (p : prop) (w : world) (e : (p@w) = true) => e.
|
|
|
|
Definition entail_trans : forall p q r : prop, (p entails q) -> (q entails r) -> (p entails r)
|
|
:= fun (p q r : prop) (f : p entails q) (g : q entails r) (w : world) (e : (p@w) = true) => g w (f w e).
|
|
|
|
Definition p_and_e1 : forall p q : prop, (p and q) entails p
|
|
:= fun (p q : prop) (w : world) (e : ((p and q)@w) = true) =>
|
|
(if (p@w) as b return ((b && (q@w)) = true -> b = true)
|
|
then (fun u : (q@w) = true => eq_refl)
|
|
else (fun v : false = true => v))
|
|
(eq_trans' (p_and_ax p q w) e).
|
|
|
|
Definition p_and_e2 : forall p q : prop, (p and q) entails q
|
|
:= fun (p q : prop) (w : world) (e : ((p and q)@w) = true) =>
|
|
(if (p@w) as b return ((b && (q@w)) = true -> (q@w) = true)
|
|
then (fun u : (q@w) = true => u)
|
|
else (fun v : false = true => if (q@w) as c return (c = true) then eq_refl else v))
|
|
(eq_trans' (p_and_ax p q w) e).
|
|
|
|
Definition p_and_i : forall p q r : prop, p entails q -> p entails r -> p entails (q and r)
|
|
:= fun (p q r : prop) (f : p entails q) (g : p entails r) (w : world) (e : (p@w) = true) =>
|
|
eq_trans (p_and_ax q r w) (f_equal2 andb (f w e) (g w e)).
|
|
|
|
Definition p_or_e : forall p q r : prop, p entails r -> q entails r -> (p or q) entails r
|
|
:= fun (p q r : prop) (f : p entails r) (g : q entails r) (w : world) (e : ((p or q)@w) = true) =>
|
|
(if (p@w) as b return ((p@w) = b -> (b || (q@w)) = true -> (r@w) = true)
|
|
then (fun (u : (p@w) = true) (v : true = true) => f w u)
|
|
else (fun x : (p@w) = false => g w))
|
|
eq_refl
|
|
(eq_trans' (p_or_ax p q w) e).
|
|
|
|
Definition p_or_i1 : forall p q : prop, p entails (p or q)
|
|
:= fun (p q : prop) (w : world) (e : (p@w) = true) => eq_trans (p_or_ax p q w) (f_equal (fun b : bool => b || (q@w)) e).
|
|
|
|
Definition p_or_i2 : forall p q : prop, q entails (p or q)
|
|
:= fun (p q : prop) (w : world) (e : (q@w) = true) =>
|
|
eq_trans (p_or_ax p q w) (if (p@w) as b return ((b || (q@w)) = true) then eq_refl else e).
|
|
|
|
Definition truth_top : forall p : prop, p entails truth
|
|
:= fun (p : prop) (w : world) (e : (p@w) = true) => truth_ax w.
|
|
|
|
Definition falsity_bot : forall p : prop, falsity entails p
|
|
:= fun (p : prop) (w : world) (e : (falsity@w) = true) =>
|
|
if (p@w) as b return (b = true) then eq_refl else (eq_trans' (falsity_ax w) e).
|
|
|
|
Definition p_implies_i : forall p q r : prop, (p and q) entails r -> p entails (q implies r)
|
|
:= fun (p q r : prop) (f : (p and q) entails r) (w : world) (e : (p@w) = true) =>
|
|
eq_trans (p_implies_ax q r w)
|
|
((if (q@w) as c return ((q@w) = c -> (c ~> (r@w)) = true)
|
|
then (fun u : (q@w) = true => f w (eq_trans (p_and_ax p q w) (f_equal2 andb e u)))
|
|
else (fun v : (q@w) = false => eq_refl))
|
|
eq_refl).
|
|
|
|
Definition p_implies_e : forall p q : prop, (p and (p implies q)) entails q
|
|
:= fun (p q : prop) (w : world) (e : ((p and (p implies q))@w) = true) =>
|
|
eq_trans' (eq_trans (p_implies_ax p q w) (f_equal (fun b : bool => b ~> (q@w)) (p_and_e1 p (p implies q) w e)))
|
|
(p_and_e2 p (p implies q) w e).
|
|
|
|
Definition complement : forall (p : prop) (w : world), ((p and (not p))@w) = false
|
|
:= fun (p : prop) (w : world) =>
|
|
eq_trans (eq_trans (p_and_ax p (not p) w) (f_equal (andb (p@w)) (p_not_ax p w)))
|
|
(if (p@w) as b return ((b && -~b) = false) then eq_refl else eq_refl).
|
|
|
|
Definition lem : forall (p : prop) (w : world), ((p or (not p))@w) = true
|
|
:= fun (p : prop) (w : world) =>
|
|
eq_trans (eq_trans (p_or_ax p (not p) w) (f_equal (orb (p@w)) (p_not_ax p w)))
|
|
(if (p@w) as b return ((b || -~b) = true) then eq_refl else eq_refl).
|
|
|
|
Definition dne : forall p : prop, (not (not p)) entails p
|
|
:= fun (p : prop) (w : world) (e : ((not (not p))@w) = true) =>
|
|
(if (p@w) as b return (-~(-~b) = true -> b = true) then (fun u : true = true => u) else (fun v : false = true => v))
|
|
(eq_trans' (eq_trans (p_not_ax (not p) w) (f_equal negb (p_not_ax p w))) e).
|
|
|
|
Definition p_forall_e : forall (s : statterm) (R : (Sns s) -> prop) (x : (Sns s)), (p_forall s R) entails (R x)
|
|
:= fun (s : statterm) (R : (Sns s) -> prop) (x : (Sns s)) (w : world) (e : ((p_forall s R)@w) = true) =>
|
|
proj1 (p_forall_ax s R w) e x.
|
|
|
|
Definition p_forall_i : forall (s : statterm) (R : (Sns s) -> prop) (p : prop),
|
|
(forall x : (Sns s), p entails (R x)) -> p entails (p_forall s R)
|
|
:= fun (s : statterm) (R : (Sns s) -> prop) (p : prop)
|
|
(f : forall x : (Sns s), p entails (R x)) (w : world) (e : (p@w) = true) =>
|
|
proj2 (p_forall_ax s R w) (fun x : (Sns s) => f x w e).
|
|
|
|
Definition p_exists_e : forall (s : statterm) (R : (Sns s) -> prop) (p : prop),
|
|
(forall x : (Sns s), (R x) entails p) -> (p_exists s R) entails p
|
|
:= fun (s : statterm) (R : (Sns s) -> prop) (p : prop)
|
|
(g : forall x : (Sns s), (R x) entails p) (w : world) (e : ((p_exists s R)@w) = true) =>
|
|
(if (p@w) as b return ((p@w) = b -> (p@w) = true)
|
|
then (fun c : (p@w) = true => c)
|
|
else (fun d : (p@w) = false =>
|
|
False_ind ((p@w) = true)
|
|
(proj1 (p_exists_ax s R w) e
|
|
(fun x : (Sns s) =>
|
|
(if ((R x)@w) as t return (((R x)@w) = t -> ((R x)@w) = false)
|
|
then (fun y : ((R x)@w) = true => False_ind (((R x)@w) = false) (tnf (eq_trans' (g x w y) d)))
|
|
else (fun z : ((R x)@w) = false => z))
|
|
eq_refl))))
|
|
eq_refl.
|
|
|
|
Definition p_exists_i : forall (s : statterm) (R : (Sns s) -> prop) (x : (Sns s)), (R x) entails (p_exists s R)
|
|
:= fun (s : statterm) (R : (Sns s) -> prop) (x : (Sns s)) (w : world) (e : ((R x)@w) = true) =>
|
|
proj2 (p_exists_ax s R w) (fun f : forall y : (Sns s), ((R y)@w) = false => tnf (eq_trans' e (f x))).
|
|
|
|
(* generalized version of eqw0eqev/neqw0neqev (doesn't require world to be inhabited) *)
|
|
Definition eqiseqev : forall (s : statterm) (x y : (Sns s)) (u v : world), ((p_equals s x y)@u) = ((p_equals s x y)@v)
|
|
:= fun (s : statterm) (x y : (Sns s)) (u v : world) =>
|
|
(if ((p_equals s x y)@v) as t return (((p_equals s x y)@v) = t -> ((p_equals s x y)@u) = t)
|
|
then (fun c : ((p_equals s x y)@v) = true => proj2 (p_equals_ax s x y u) (proj1 (p_equals_ax s x y v) c))
|
|
else (fun d : ((p_equals s x y)@v) = false =>
|
|
(if ((p_equals s x y)@u) as b return (((p_equals s x y)@u) = b -> b = false)
|
|
then (fun a : ((p_equals s x y)@u) = true =>
|
|
eq_trans' (proj2 (p_equals_ax s x y v) (proj1 (p_equals_ax s x y u) a)) d)
|
|
else (fun e : ((p_equals s x y)@u) = false => eq_refl))
|
|
eq_refl))
|
|
eq_refl.
|
|
|
|
(* These last 3 axioms requires that world is inhabited, specifically by a term w0 *)
|
|
|
|
Definition nondeg : ~(truth ≡ falsity)
|
|
:= and_ind (fun (f : truth entails falsity) (g : falsity entails truth) =>
|
|
tnf (eq_trans' (f w0 (truth_ax w0)) (falsity_ax w0))).
|
|
|
|
Definition eq_one : forall (s : statterm) (x y : (Sns s)), ((p_equals s x y) ≡ truth) \/ ((p_equals s x y) ≡ falsity)
|
|
:= fun (s : statterm) (x y : (Sns s)) =>
|
|
(if ((p_equals s x y)@w0) as b
|
|
return (((p_equals s x y)@w0) = b -> ((p_equals s x y) ≡ truth) \/ ((p_equals s x y) ≡ falsity))
|
|
then (fun c : ((p_equals s x y)@w0) = true =>
|
|
or_introl (conj (truth_top (p_equals s x y))
|
|
(fun (v : world) (e : (truth@v) = true) => eq_trans' (eqiseqev s x y w0 v) c)))
|
|
else (fun d : ((p_equals s x y)@w0) = false =>
|
|
or_intror (conj (fun (v : world) (e : ((p_equals s x y)@v) = true) =>
|
|
if (falsity@v) as t return (t = true)
|
|
then eq_refl
|
|
else (eq_trans' d (eq_trans (eqiseqev s x y w0 v) e)))
|
|
(falsity_bot (p_equals s x y)))))
|
|
eq_refl.
|
|
|
|
Definition eq_two : forall (s : statterm) (x y : (Sns s)), ((p_equals s x y) ≡ truth) <-> (x = y)
|
|
:= fun (s : statterm) (x y : (Sns s)) =>
|
|
conj (and_ind (fun (f : (p_equals s x y) entails truth) (g : truth entails (p_equals s x y)) =>
|
|
proj1 (p_equals_ax s x y w0) (g w0 (truth_ax w0))))
|
|
(fun e : x = y => conj (truth_top (p_equals s x y))
|
|
(fun (u : world) (c : (truth@u) = true) => proj2 (p_equals_ax s x y u) e)).
|
|
End prop_Theorems.
|
|
|
|
(* basically showing that ≡_p implies mutual entailment *)
|
|
Definition int_eq : forall p q : prop, (forall w : world, (p@w) = (q@w)) -> p ≡ q
|
|
:= fun (p q : prop) (f : forall w : world, (p @ w) = (q @ w)) =>
|
|
conj (fun w : world => eq_trans' (f w)) (fun w : world => eq_trans (f w)).
|
|
|
|
(* duality of prop quantifiers *)
|
|
Definition comp : forall {A B C:Type},(B->C)->(A->B)->A->C := fun (A B C : Type) (f : B -> C) (g : A -> B) (x : A) => f (g x).
|
|
Infix "∘" := comp (at level 20).
|
|
Definition dubneg : forall b : bool, b = -~(-~b) := bool_ind (fun b : bool => b = -~(-~b)) eq_refl eq_refl.
|
|
|
|
Section QuantifierDuals.
|
|
Hypotheses (s : statterm) (P : Sns s -> prop).
|
|
Definition qudupr1 : (p_exists s P) ≡ (not (p_forall s (p_not∘P)))
|
|
:= conj (fun (w : world) (d : ((p_exists s P)@w) = true) =>
|
|
eq_trans (p_not_ax (p_forall s (p_not∘P)) w)
|
|
(f_equal negb
|
|
((if ((p_forall s (p_not∘P))@w) as b return (((p_forall s (p_not∘P))@w) = b -> b = false)
|
|
then (fun e : ((p_forall s (p_not∘P))@w) = true =>
|
|
False_ind (true = false)
|
|
(proj1 (p_exists_ax s P w) d
|
|
(fun x : Sns s =>
|
|
eq_trans (dubneg ((P x)@w))
|
|
(f_equal negb
|
|
(eq_trans' (p_not_ax (P x) w)
|
|
(proj1 (p_forall_ax s (p_not∘P) w) e x))))))
|
|
else (fun _ : ((p_forall s (p_not∘P))@w) = false => eq_refl))
|
|
eq_refl)))
|
|
(fun (w : world) (d : (((not p_forall s (p_not∘P)))@w) = true) =>
|
|
proj2 (p_exists_ax s P w)
|
|
(fun f : forall x : Sns s, (P x @ w) = false =>
|
|
tnf (eq_trans'
|
|
(proj2 (p_forall_ax s (p_not∘P) w)
|
|
(fun x : Sns s => eq_trans (p_not_ax (P x) w) (f_equal negb (f x))))
|
|
(eq_trans (dubneg ((p_forall s (p_not∘P))@w))
|
|
(f_equal negb (eq_trans' (p_not_ax (p_forall s (p_not∘P)) w) d)))))).
|
|
Definition qudupr2 : (p_forall s P) ≡ (not (p_exists s (p_not∘P)))
|
|
:= conj (fun (w : world) (d : ((p_forall s P)@w) = true) =>
|
|
eq_trans (p_not_ax (p_exists s (p_not∘P)) w)
|
|
(f_equal negb
|
|
((if ((p_exists s (p_not∘P))@w) as b return ((p_exists s (p_not ∘ P) @ w) = b -> b = false)
|
|
then (fun e : ((p_exists s (p_not∘P))@w) = true =>
|
|
False_ind (true = false)
|
|
(proj1 (p_exists_ax s (p_not∘P) w) e
|
|
(fun x : Sns s =>
|
|
eq_trans (p_not_ax (P x) w)
|
|
(f_equal negb (proj1 (p_forall_ax s P w) d x)))))
|
|
else (fun _ : ((p_exists s (p_not∘P))@w) = false => eq_refl))
|
|
eq_refl)))
|
|
(fun (w : world) (d : ((not (p_exists s (p_not∘P)))@w) = true) =>
|
|
proj2 (p_forall_ax s P w)
|
|
(fun x : Sns s =>
|
|
(if ((P x)@w) as b return (((P x)@w) = b -> b = true)
|
|
then (fun _ : (P x @ w) = true => eq_refl)
|
|
else (fun e : (P x @ w) = false =>
|
|
eq_trans'
|
|
(eq_trans (dubneg ((p_exists s (p_not∘P))@w))
|
|
(f_equal negb (eq_trans' (p_not_ax (p_exists s (p_not∘P)) w) d)))
|
|
(proj2 (p_exists_ax s (p_not∘P) w)
|
|
(fun f : forall y : Sns s, ((not (P y))@w) = false =>
|
|
tnf (eq_trans' (eq_trans (p_not_ax (P x) w) (f_equal negb e))
|
|
(f x))))))
|
|
eq_refl)).
|
|
Definition qudupr3 : (p_exists s (p_not∘P)) ≡ (not (p_forall s P))
|
|
:= conj (fun (w : world) (d : ((p_exists s (p_not∘P))@w) = true) =>
|
|
eq_trans (p_not_ax (p_forall s P) w)
|
|
(f_equal negb
|
|
((if ((p_forall s P)@w) as b return (((p_forall s P)@w) = b -> b = false)
|
|
then (fun e : (p_forall s P @ w) = true =>
|
|
False_ind (true = false)
|
|
(proj1 (p_exists_ax s (p_not∘P) w) d
|
|
(fun x : Sns s =>
|
|
eq_trans (p_not_ax (P x) w)
|
|
(f_equal negb (proj1 (p_forall_ax s P w) e x)))))
|
|
else (fun _ : ((p_forall s P)@w) = false => eq_refl))
|
|
eq_refl)))
|
|
(fun (w : world) (d : ((not (p_forall s P))@w) = true) =>
|
|
proj2 (p_exists_ax s (p_not∘P) w)
|
|
(fun f : forall x : Sns s, ((p_not∘P) x @ w) = false =>
|
|
tnf (eq_trans'
|
|
(proj2 (p_forall_ax s P w)
|
|
(fun x : Sns s =>
|
|
eq_trans (dubneg ((P x)@w))
|
|
(f_equal negb (eq_trans' (p_not_ax (P x) w) (f x)))))
|
|
(eq_trans (dubneg ((p_forall s P)@w))
|
|
(f_equal negb (eq_trans' (p_not_ax (p_forall s P) w) d)))))).
|
|
Definition qudupr4 : (p_forall s (p_not∘P)) ≡ (not (p_exists s P))
|
|
:= conj (fun (w : world) (d : ((p_forall s (p_not∘P))@w) = true) =>
|
|
eq_trans (p_not_ax (p_exists s P) w)
|
|
(f_equal negb
|
|
((if ((p_exists s P)@w) as b return (((p_exists s P)@w) = b -> b = false)
|
|
then (fun e : ((p_exists s P)@w) = true =>
|
|
False_ind (true = false)
|
|
(proj1 (p_exists_ax s P w) e
|
|
(fun x : Sns s =>
|
|
eq_trans (dubneg ((P x)@w))
|
|
(f_equal negb
|
|
(eq_trans' (p_not_ax (P x) w)
|
|
(proj1 (p_forall_ax s (p_not∘P) w) d x))))))
|
|
else (fun _ : ((p_exists s P)@w) = false => eq_refl))
|
|
eq_refl)))
|
|
(fun (w : world) (d : ((not (p_exists s P))@w) = true) =>
|
|
proj2 (p_forall_ax s (p_not∘P) w)
|
|
(fun x : Sns s =>
|
|
eq_trans (p_not_ax (P x) w)
|
|
(f_equal negb
|
|
((if ((P x)@w) as b return (((P x)@w) = b -> b = false)
|
|
then
|
|
(fun e : ((P x)@w) = true =>
|
|
eq_trans' (proj2 (p_exists_ax s P w)
|
|
(fun f : forall y : Sns s, ((P y)@w) = false =>
|
|
tnf (eq_trans' e (f x))))
|
|
(eq_trans (dubneg ((p_exists s P)@w))
|
|
(f_equal negb
|
|
(eq_trans' (p_not_ax (p_exists s P) w) d))))
|
|
else (fun _ : ((P x)@w) = false => eq_refl))
|
|
eq_refl)))).
|
|
End QuantifierDuals.
|
|
|
|
|
|
|
|
|