search

Ayertienna / IS5

Intuitionistic S5 logic formalization
4 stars 0 forks source link

Decision procedure: permut #38

Closed Ayertienna closed 11 years ago

Ayertienna commented 12 years ago

{ permut l1 l2} + {~ permut l1 l2} -- should this be a lemma or can we just add it as an axiom?

problem: induction step when two new elements are not equal -- so HT: forall l2, {permut l1 l2} + {~permut l1 l2} TS: {permut a::l1 b::l2} {~ permut a::l1 b::l2} having a <> b

Ayertienna commented 11 years ago

Ok, this is simple when we want a boolean value out of it, so: permut l1 l2 \/ ~ permut l1 l2. In the { } + { } case there is a problem: a::l1 = l2 when Mem a l2 and we have l2 as hd & a ++ tl and l1 = hd ++ tl (from IH). But as long as we're proving { } + { } goal, we cannot destruct the result of Mem_split into hd and tl..

Ayertienna commented 11 years ago

Completely fixed.