i'm using couple of inductive definitions counter examples in proofs. encapsulate these definitions enclosing them in section. regular definitions can hidden using let, possible inductive definitions? , how theorems?
let me give actual thing i'm trying achieve, may going totally wrong way in first place. want formalize proofs , exercises of excellent book "logics of time , computation" robert goldblatt coq.
for starters take classical logic book well.
require import classical_prop. require import classical_pred_type. next define identifiers same way done in software foundations.
inductive id : type := id : nat -> id. definition of syntax.
inductive modal : type := | bottom : modal | v : id -> modal | imp : modal -> modal -> modal | box : modal -> modal . definition not (f : modal) : modal := imp f bottom. definition of semantics using kripke frames.
(* inspired by: www.cs.vu.nl/~tcs/mt/dewind.ps.gz *) record frame : type := { worlds : type ; worldsexist : exists w : worlds, true ; rel : worlds -> worlds -> prop }. record kripke : type := { frame : frame ; label : (worlds frame) -> id -> prop }. fixpoint satisfies (m : kripke) (x : (worlds (frame m))) (f : modal) : prop := match f | bottom => false | v v => (label m x v) | imp f1 f2 => (satisfies m x f1) -> (satisfies m x f2) | box f => forall y : (worlds (frame m)), (rel (frame m) x y) -> (satisfies m y f) end. the first lemma relates modal not 1 of coq.
lemma satisfies_not : forall m x f , satisfies m x (not f) = ~ satisfies m x f . proof. auto. qed. next lift semantics complete models.
definition m_satisfies (m : kripke) (f : modal) : prop := forall w : worlds (frame m), satisfies m w f. and show means not connective.
lemma m_satisfies_not : forall m f , m_satisfies m (not f) -> ~ m_satisfies m f . proof. unfold m_satisfies. intros m f hn hcontra. destruct (worldsexist (frame m)). specialize (hn x); clear h. rewrite satisfies_not in hn. specialize (hcontra x). auto. qed. here comes thing. reverse of above lemma not hold , want show counter example, exhibiting model doesn't hold.
inductive wcounter : set := | x1:wcounter | x2:wcounter | x3:wcounter. lemma wcounter_not_empty : exists w : wcounter, true. proof. exists x1. constructor. qed. inductive rcounter (x : wcounter) (y : wcounter) : prop := | e1 : x = x1 -> y = x2 -> rcounter x y | e2 : x = x2 -> y = x3 -> rcounter x y . definition lcounter : wcounter -> id -> prop := fun x => match x | x1 => match | id 0 => true | _ => false end | x2 => match | id 1 => true | _ => false end | x3 => match | id 0 => true | _ => false end end. definition fcounter : frame := build_frame wcounter wcounter_not_empty rcounter. definition kcounter : kripke := build_kripke fcounter lcounter. next ltac relieves me typing verbose asserts.
ltac counter_example h hc := match type of h | ?p -> ~ ?q => assert(hc: q) | ?p -> (?q -> false) => assert(hc: q) | ?p -> ?q => assert(hc: ~q) end. finally use counter example prove following lemma.
lemma m_not_satisfies_not : ~ forall m f , (~ m_satisfies m f) -> m_satisfies m (not f) . proof. apply ex_not_not_all. exists kcounter. apply ex_not_not_all. exists (v (id 0)). unfold m_satisfies. simpl. intro hcontra. unfold not in hcontra. counter_example hcontra hn2. apply ex_not_not_all. exists x1. simpl. auto. apply hn2. apply hcontra. apply ex_not_not_all; exists x2. simpl. auto. qed. preferably have used remember tactic define counter example inside proof, don't think can used inductive definitions. definitions relating counter example exported part of theory, prefer not do. used in proof of m_not_satisfies_not. not want export lemma either not useful. put there argue m_satisfies_not can not equivalence.
section doesn't hide definitions, use module instead. example put counter example in module.
module counterexample. import definitions. inductive wcounter : set := x1 | x2 | x3. ... lemma m_not_satisfies_not : ... end counterexample. at stage, counterexample defined @ top level.
if don't want either, put definitions in 1 .v file , counter example in file imports definitions. actually, way works .v files turned individual modules.
Comments
Post a Comment