From d8ab88f926134731baa64f48c519289587c20261 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 23 Jul 2010 09:25:06 +0000 Subject: [PATCH] Some experiments on a co-inductive Heityng algebra. --- .../software/matita/nlibrary/logic/cologic.ma | 253 ++++++++++++++++++ 1 file changed, 253 insertions(+) create mode 100644 helm/software/matita/nlibrary/logic/cologic.ma diff --git a/helm/software/matita/nlibrary/logic/cologic.ma b/helm/software/matita/nlibrary/logic/cologic.ma new file mode 100644 index 000000000..474eab726 --- /dev/null +++ b/helm/software/matita/nlibrary/logic/cologic.ma @@ -0,0 +1,253 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "logic/pts.ma". +include "logic/equality.ma". + +ncoinductive cprop: Type[0] ≝ + false: cprop + | true: cprop + | maybe: cprop → cprop. + +ntheorem ccases: + ∀c. c = match c with [ false ⇒ false | true ⇒ true | maybe c ⇒ maybe c ]. + #c; ncases c; //. +nqed. + +ninductive cconv : cprop → cprop → CProp[0] ≝ + true_true: cconv true true + | false_false: cconv false false + | maybe1: ∀c1,c2. cconv c1 c2 → cconv (maybe c1) c2 + | maybe2: ∀c1,c2. cconv c1 c2 → cconv c1 (maybe c2). + +ncoinductive cdiv: cprop → cprop → CProp[0] ≝ + cdodiv: ∀c,d. cdiv c d → cdiv (maybe c) (maybe d). + +ndefinition cdiv1: ∀c. cdiv (maybe false) c → False. + #c K; ninversion K; #a b K1 K2 K3; ndestruct; ninversion K1; #; ndestruct. +nqed. + +ndefinition cdiv2: ∀c. cdiv (maybe true) c → False. + #c K; ninversion K; #a b K1 K2 K3; ndestruct; ninversion K1; #; ndestruct. +nqed. + +ndefinition cdiv3: ∀c. cdiv c false → False. + #c K; ninversion K; #; ndestruct. +nqed. + +ndefinition cdiv4: ∀c. cdiv c true → False. + #c K; ninversion K; #; ndestruct. +nqed. + +nlet corec cdiv5 c d (K: cdiv (maybe c) d) : cdiv c d ≝ ?. + ngeneralize in match K; ncases c + [ #E; ncases (cdiv1 … E) + | #E; ncases (cdiv2 … E) + | ncases d + [ #e E; ncases (cdiv3 … E) + | #e E; ncases (cdiv4 … E) + | #x y K1; @; napply cdiv5; ninversion K1; #; ndestruct; nassumption]##] +nqed. + +nlemma cconv_cdiv_false: ∀c,d,e. cconv c e → cdiv c d → False. + #c d e K; nelim K + [##1,2: #U; ninversion U; #; ndestruct + |##*: /3/] +nqed. + +ndefinition ceq ≝ λc1,c2. cconv c1 c2 ∨ cdiv c1 c2. + +ndefinition committed ≝ λc. ceq c c. + +nrecord cval : Type[0] ≝ { + ccarr:> cprop; + ccomm: committed ccarr +}. + +ntheorem ceq_refl: ∀c:cval. ceq c c. + //. +nqed. + +nlet corec cdiv_sym c d (K: cdiv c d) : cdiv d c ≝ ?. + ncases K; /3/. +nqed. + +nlet rec cconv_sym c d (K: cconv c d) on K : cconv d c ≝ ?. + ncases K; /3/. +nqed. + +ntheorem ceq_sym: ∀c,d:cval. ceq c d → ceq d c. + #x; ncases x; #c Kc; #y; ncases y; #d Kd; + ncases Kc; #K1; *; /3/. +nqed. + +nlet corec cand c1 c2 : cprop ≝ + match c1 with + [ false ⇒ false + | true ⇒ c2 + | maybe c ⇒ + match c2 with + [ false ⇒ false + | true ⇒ maybe c + | maybe d ⇒ maybe (cand c d) ]]. + +nlemma cand_false: ∀c. cand false c = false. + #c; ncases c; nrewrite > (ccases (cand …)); //; #d; + nrewrite > (ccases (cand …)); //. +nqed. + +nlemma cand_true: ∀c. cand true c = c. + #c; ncases c; nrewrite > (ccases (cand \ldots)); //; #d; + nrewrite > (ccases (cand …)); //. +nqed. + +ntheorem cand_true: ∀c1,c2. ceq c1 true → ceq (cand c1 c2) c2. + #c1 c2 K; ncases K + [##2: #X; ncases (cdiv4 … X) + | #E; ninversion E (* induction inversion qui *) + [ #_; #_; nrewrite > (cand_true …); napply ceq_refl; + | + + +ncoinductive cprop: Type[0] ≝ + false: cprop + | true: cprop + | hmm: cprop → cprop. + +nlet corec cand c1 c2 : cprop ≝ + match c1 with + [ false ⇒ false + | true ⇒ c2 + | hmm c ⇒ hmm (cand c c2) ]. + +nlet corec cor c1 c2 : cprop ≝ + match c1 with + [ false ⇒ c2 + | true ⇒ true + | hmm c ⇒ hmm (cor c c2) ]. + +nlet corec cimpl c1 c2 : cprop ≝ + match c2 with + [ false ⇒ + match c1 with + [ false ⇒ true + | true ⇒ false + | hmm c ⇒ hmm (cimpl c c2) ] + | true ⇒ true + | hmm c ⇒ hmm (cimpl c1 c) ]. + +include "Plogic/equality.ma". + +nlet corec ceq c1 c2 : cprop ≝ + match c1 with + [ false ⇒ + match c2 with + [ false ⇒ true + | true ⇒ false + | hmm c ⇒ hmm (ceq c1 c) ] + | true ⇒ c2 + | hmm c ⇒ hmm (ceq c c2) ]. + +ninductive holds: cprop → Prop ≝ + holds_true: holds true + | holds_hmm: ∀c. holds c → holds (hmm c). + +include "Plogic/connectives.ma". + +nlemma ccases1: + ∀c. holds c → + match c with + [ true ⇒ True + | false ⇒ False + | hmm c' ⇒ holds c']. + #c; #H; ninversion H; //. +nqed. + +nlemma ccases2: + ∀c. + match c with + [ true ⇒ True + | false ⇒ False + | hmm c' ⇒ holds c'] → holds c ≝ ?. + #c; ncases c; nnormalize; /2/; *. +nqed. + +(*CSC: ??? *) +naxiom cimpl1: ∀c. holds (cimpl true c) → holds c. + +nlemma ceq1: ∀c. holds c → holds (ceq c true). + #c H; nelim H; /2/. +nqed. + +ncoinductive EQ: cprop → cprop → Prop ≝ + EQ_true: EQ true true + | EQ_false: EQ false false + | EQ_hmm1: ∀x,y. EQ x y → EQ (hmm x) y + | EQ_hmm2: ∀x,y. EQ x y → EQ x (hmm y). + +naxiom daemon: False. + +nlet corec tech1 x: ∀y. EQ (hmm x) y → EQ x y ≝ ?. + #y; ncases y + [##1,2: #X; ninversion X; #; ndestruct; // + | #c; #X; ninversion X; #; ndestruct; //; + @4; ncases daemon (* napply tech1; //*) (* BUG GBC??? *) + ] +nqed. + +nlemma Ccases1: + ∀c,d. EQ c d → + match c with + [ true ⇒ EQ true d + | false ⇒ EQ false d + | hmm c' ⇒ EQ c' d] ≝ ?. + #c d H; ninversion H; //; + #x y H H1 H2; ndestruct; ncases x in H ⊢ %; nnormalize; #; @4; //; + napply tech1; //. +nqed. + +nlemma Ccases2: + ∀c,d. + match c with + [ true ⇒ EQ true d + | false ⇒ EQ false d + | hmm c' ⇒ EQ c' d] → EQ c d ≝ ?. + #c; ncases c; nnormalize; /2/. +nqed. + +nlet corec heyting5 x: ∀y. EQ (cimpl (cand x y) x) true ≝ ?. + #y; napply Ccases2; ncases x; ncases y; nnormalize; /3/ + [ #c; napply heyting5; + + +nlemma heyting3: ∀x,y. holds (cimpl x (cimpl y x)). + #x; #y; ncases x; ncases y; /3/; nnormalize + [ #d; napply ccases2; nnormalize; napply ccases2; nnormalize; + +nlemma heyting1: ∀x,y. holds (cimpl x y) → holds (cimpl y x) → holds (ceq x y). + #x y; #H; ngeneralize in match (refl … (cimpl x y)); + nelim H in ⊢ (???% → % → %) + [ #K1; #K2; nrewrite > K1 in K2; #X1; + + napply ccases2; nlapply (ccases1 … H1); nlapply (ccases1 … H2); + ncases x; ncases y; nnormalize; /2/ + [ #c; #H3 H4; nlapply (cimpl1 … H3); napply ceq1 + | #d; #e; #H3; #H4; + + ncases x; nnormalize + [ #y; ncases y; // + | #y; ncases y; // + [ #H1; ninversion H1; ##[##1,4: #; ndestruct] + ##[ ncases (cimpl true false); + [ ninversion H1; #; ndestruct; \ No newline at end of file -- 2.39.2