API tools faq
paste
SkullCoder

Coq AR Ex 2.4

SkullCoder
Nov 11th, 2019
179
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
JavaScript 6.53 KB | None | 0 0
raw download clone embed print report
  1. Require Import List Lia.
  2. Require Import String.
  3. Import ListNotations Nat.
  4. Open Scope string.
  5. Open Scope nat_scope.
  6.  
  7. Inductive formula {Pi} :=
  8.   Bot | Top | V (p:Pi) | Not (a:formula) |
  9.   And (a b:formula) | Or (a b:formula) |
  10.   To (a b:formula) | Equiv (a b:formula).
  11.  
  12. Definition app {X} {Y} (f:X->Y) (x:option X) : option Y :=
  13.   match x with
  14.     None => None
  15.   | Some x => Some (f x)
  16.   end.
  17.  
  18. Notation "F ∨ G" := (Or F G)(at level 71).
  19. Notation "F ∧ G" := (And F G)(at level 71).
  20. Notation "F → G" := (To F G)(at level 71).
  21. Notation "F ↔ G" := (Equiv F G)(at level 71).
  22. Notation "¬ F" := (Not F)(at level 70).
  23.  
  24.  
  25. Definition StringVar := @V string.
  26. Coercion StringVar : string >-> formula.
  27.  
  28. Definition testFormula :=
  29.   "P" ∨ (¬"Q" → (¬ "P" ∧ Top)).
  30. (* Compute (negvar testFormula). *)
  31.  
  32.  
  33. Fixpoint subst {Pi} (F G:@formula Pi) p :=
  34.   match F, p with
  35.     _, [] => Some G
  36.   | (Not F), 1::p => app Not (subst F G p)
  37.   | (And F1 F2), 1::p => app (fun f => And f F2) (subst F1 G p)
  38.   | (And F1 F2), 2::p => app (And F1) (subst F2 G p)
  39.   | (Or F1 F2), 1::p => app (fun f => Or f F2) (subst F1 G p)
  40.   | (Or F1 F2), 2::p => app (Or F1) (subst F2 G p)
  41.   | (To F1 F2), 1::p => app (fun f => To f F2) (subst F1 G p)
  42.   | (To F1 F2), 2::p => app (To F1) (subst F2 G p)
  43.   | (Equiv F1 F2), 1::p => app (fun f => Equiv f F2) (subst F1 G p)
  44.   | (Equiv F1 F2), 2::p => app (Equiv F1) (subst F2 G p)
  45.   | _, _ => None
  46.   end.
  47.  
  48. Inductive polarity := TT | FF | NN.
  49.  
  50. Definition negPol p :=
  51.   match p with
  52.     TT => FF
  53.   | FF => TT
  54.   | NN => NN
  55.   end.
  56.  
  57. Fixpoint pol {Pi} (F:@formula Pi) p :=
  58.   match F,p with
  59.     _, [] => Some TT
  60.   | (Not F), 1::p => app negPol (pol F p)
  61.   | (And F1 F2), 1::p => pol F1 p
  62.   | (And F1 F2), 2::p => pol F2 p
  63.   | (Or F1 F2), 1::p => pol F1 p
  64.   | (Or F1 F2), 2::p => pol F2 p
  65.   | (To F1 F2), 1::p => app negPol (pol F1 p)
  66.   | (To F1 F2), 2::p => pol F2 p
  67.   | (Equiv F1 F2), 1::p => Some NN
  68.   | (Equiv F1 F2), 2::p => Some NN
  69.   | _,_ => None
  70.   end.
  71.  
  72. Definition bool2nat (b:bool) := if b then 1 else 0.
  73.  
  74. Coercion bool2nat : bool >-> nat.
  75.  
  76. Fixpoint eval {Pi} (A:Pi->bool) (F:@formula Pi) : nat :=
  77.   match F with
  78.     Bot => 0
  79.   | Top => 1
  80.   | V p => A p
  81.   | Not F => 1-eval A F
  82.   | And F G => min (eval A F) (eval A G)
  83.   | Or F G => max (eval A F) (eval A G)
  84.   | To F G => max (1-eval A F) (eval A G)
  85.   | Equiv F G => if eval A F =? eval A G then 1 else 0
  86.   end.
  87.  
  88.  
  89. Lemma polEmpty {Pi} (H:@formula Pi) : pol H [] = Some TT.
  90. Proof.
  91.   destruct H;reflexivity.
  92. Qed.
  93.  
  94. Lemma substEmpty {Pi} (H F:@formula Pi) : subst H F [] = Some F.
  95. Proof.
  96.   destruct H;reflexivity.
  97. Qed.
  98.  
  99. Lemma appInv {X Y} (f:X->Y) x b: app f x = Some b <-> exists a, x=Some a /\ b=f a.
  100. Proof.
  101.   unfold app.
  102.   split.
  103.   - intros H. destruct x.
  104.     + exists x;split;congruence.
  105.     + congruence.
  106.   - intros (a&H0&H1). now subst.
  107. Qed.
  108.  
  109. Goal forall Pi A (F G H:@formula Pi) p, forall hf hg, subst H F p = Some hf -> subst H G p = Some hg ->
  110.     (pol H p = Some TT -> eval A F <= eval A G -> eval A hf <= eval A hg) /\
  111.     (pol H p = Some FF -> eval A F >= eval A G -> eval A hf <= eval A hg).
  112. Proof.
  113.   intros Pi A F G H p.
  114.   induction p in F, G, H |- *.
  115.   - intros. rewrite polEmpty. split;intros.
  116.     + rewrite substEmpty in H0, H1.
  117.       injection H0 as <-;injection H1 as <-.
  118.       exact H3.
  119.     + congruence.
  120.   - intros hf hg Ef Eg.
  121.     destruct H as [ | | |H'|H1 H2|H1 H2|H1 H2|H1 H2] eqn:H0;
  122.      destruct a as [|[|[|]]];cbn in *;try congruence.
  123.    all: rewrite appInv in Ef,Eg;
  124.      destruct Ef as (af&Ef0&->);
  125.      destruct Eg as (ag&Eg0&->).
  126.  
  127.    (* ~ *)
  128.    + destruct pol as [[]|] eqn:Hp;cbn;split;intros;try congruence.
  129.      all: destruct (IHp G F H' ag af Eg0 Ef0).
  130.       1: specialize (H3 Hp H2).
  131.       2: specialize (H4 Hp H2).
  132.       all: destruct (eval A af), (eval A ag);repeat constructor;
  133.         now apply PeanoNat.Nat.nle_succ_0 in H3.
  134.  
  135.     (* /\ *)
  136.     (* second case is like first case but with H2 in IH *)
  137.     + destruct (IHp F G H1 af ag Ef0 Eg0).
  138.       destruct pol as [[]|];split;intros;try congruence;cbn.
  139.       * specialize (H3 H5 H6).
  140.         now apply PeanoNat.Nat.min_le_compat.
  141.       * specialize (H4 H5 H6).
  142.         now apply PeanoNat.Nat.min_le_compat.
  143.     + destruct (IHp F G H2 af ag Ef0 Eg0).
  144.       destruct pol as [[]|];split;intros;try congruence;cbn.
  145.       * specialize (H3 H5 H6).
  146.         now apply PeanoNat.Nat.min_le_compat.
  147.       * specialize (H4 H5 H6).
  148.         now apply PeanoNat.Nat.min_le_compat.
  149.  
  150.     (* \/ *)
  151.     (* /\ but with max instead of min *)
  152.     + destruct (IHp F G H1 af ag Ef0 Eg0).
  153.       destruct pol as [[]|];split;intros;try congruence;cbn.
  154.       * specialize (H3 H5 H6).
  155.         now apply PeanoNat.Nat.max_le_compat.
  156.       * specialize (H4 H5 H6).
  157.         now apply PeanoNat.Nat.max_le_compat.
  158.     + destruct (IHp F G H2 af ag Ef0 Eg0).
  159.       destruct pol as [[]|];split;intros;try congruence;cbn.
  160.       * specialize (H3 H5 H6).
  161.         now apply PeanoNat.Nat.max_le_compat.
  162.       * specialize (H4 H5 H6).
  163.         now apply PeanoNat.Nat.max_le_compat.
  164.  
  165.     (* -> *)
  166.     (* first case is ~ \/ *)
  167.     (* first case is \/ *)
  168.     + destruct (IHp G F H1 ag af Eg0 Ef0).
  169.       destruct pol as [[]|];split;intros [=] ?.
  170.       1: apply H3 in H6;trivial.
  171.       2: apply H4 in H6;trivial.
  172.       all: cbn;
  173.       apply PeanoNat.Nat.max_le_compat;
  174.       destruct (eval A af), (eval A ag);lia.
  175.     + destruct (IHp F G H2 af ag Ef0 Eg0).
  176.       destruct pol as [[]|];split;intros [=] ?.
  177.       1: apply H3 in H6;trivial.
  178.       2: apply H4 in H6;trivial.
  179.       all: now cbn;apply PeanoNat.Nat.max_le_compat.
  180.  
  181.     (* <-> no case applicable *)
  182.     + split;intros [=].
  183.     + split;intros [=].
  184. Qed.
  185.  
  186.  
  187.  
  188.  
  189.  
  190. Fixpoint negvar {Pi} (F:@formula Pi) :=
  191.   match F with
  192.     V p => Not (V p)
  193.   | Not f => Not (negvar f)
  194.   | And f1 f2 => And (negvar f1) (negvar f2)
  195.   | Or f1 f2 => Or (negvar f1) (negvar f2)
  196.   | To f1 f2 => To (negvar f1) (negvar f2)
  197.   | Equiv f1 f2 => Equiv (negvar f1) (negvar f2)
  198.   | _ => F
  199.   end.
  200.  
  201. Definition satisfiable {Pi} (F:@formula Pi) : Prop :=
  202.   exists A, eval A F = 1.
  203.  
  204. Lemma negvarEval: forall X (F:@formula X) A, eval A F = eval (fun a => negb (A a)) (negvar F).
  205. Proof.
  206.   intros Pi F A.
  207.   induction F;cbn;trivial;intros.
  208.   all: try(now destruct (eval A F1), (eval A F2);rewrite <- IHF1, <- IHF2).
  209.   - now destruct A.
  210.   - now destruct eval;rewrite <- IHF.
  211. Qed.
  212.  
  213. Goal forall X (F:@formula X), satisfiable F -> satisfiable (negvar F).
  214. Proof.
  215.   intros Pi F [A H].
  216.   exists (fun a => negb (A a)).
  217.   now rewrite <- negvarEval.
  218. Qed.
Advertisement
Add Comment
Please, Sign In to add comment
Public Pastes
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.  OK, I Understand
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!