-
Notifications
You must be signed in to change notification settings - Fork 0
/
project3.v
1595 lines (1456 loc) · 60.8 KB
/
project3.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
Require Export List Omega.
Import ListNotations.
From icl Require Import util assignments formulas number_of_models.
(** * Algorithm 1 *)
(* Algorithm 1 just computes all the possible assignments
and then filters all non-satisfying assignments. *)
Section Algorithm1.
(* Generate all the possible assignments on a given set of variables. *)
Fixpoint all_assignments_on (vs : variables) : assignments :=
match vs with
| [] => [[]] | v::vs =>
map (cons (v,false)) (all_assignments_on vs) ++
map (cons (v,true)) (all_assignments_on vs)
end.
Lemma vars_of_assignment_in_all_assignments_on:
forall (vs : variables) (α : assignment),
α el all_assignments_on vs ->
equi (vars_in α) vs.
Proof.
induction vs; intros ? EL; simpl in EL.
- destruct EL as [EL|F]; [subst |exfalso]; auto.
split; intros x EL; destruct EL.
- apply in_app_iff in EL; destruct EL as [EL|EL].
+ apply in_map_iff in EL; destruct EL as [α_tl [EQ EL]]; subst α.
specialize (IHvs _ EL); simpl; auto using equi_cons.
+ apply in_map_iff in EL; destruct EL as [α_tl [EQ EL]]; subst α.
specialize (IHvs _ EL); simpl; auto using equi_cons.
Qed.
Corollary assignment_in_all_assignments_on_sets_all_variables:
forall (ϕ : formula) (α : assignment),
α el all_assignments_on (formula_vars ϕ) ->
sets_all_variables α ϕ.
Proof.
intros ? ? EL.
apply vars_of_assignment_in_all_assignments_on in EL; rename EL into EQU.
intros v EL; apply EQU.
apply nodup_In; assumption.
Qed.
Lemma size_of_list_of_all_assignments_on:
forall (vs : variables),
length (all_assignments_on vs) = Nat.pow 2 (length vs).
Proof.
induction vs; simpl; auto.
rewrite app_length, !map_length, <- plus_n_O, <- IHvs; auto.
Qed.
Lemma list_of_all_assignments_dupfree:
forall (vs : variables),
NoDup vs ->
dupfree vs (all_assignments_on vs).
Proof.
intros ? ND; split.
{ induction vs.
- constructor; [intros C; easy | constructor ].
- apply NoDup_cons_iff in ND; destruct ND as [NEL ND].
feed IHvs; [assumption | ].
apply nodup_app_of_map_cons; easy.
}
{ induction vs; intros α1 α2 EL1 EL2 NEQ EQ.
{ inversion EL1; inversion EL2; subst; auto. }
{ apply NoDup_cons_iff in ND; destruct ND as [NEL ND].
feed IHvs; auto.
simpl in EL1, EL2; apply in_app_iff in EL1; apply in_app_iff in EL2.
destruct EL1 as [EL1|EL1], EL2 as [EL2|EL2];
apply in_map_iff in EL1; apply in_map_iff in EL2;
destruct EL1 as [α1_tl [EQ1 EL1]], EL2 as [α2_tl [EQ2 EL2]].
{ rewrite <-EQ1, <-EQ2 in EQ, NEQ; clear EQ1 EQ2 α1 α2.
rename α1_tl into α1, α2_tl into α2.
apply neq_cons in NEQ.
specialize (IHvs _ _ EL1 EL2 NEQ).
apply IHvs; clear IHvs.
eapply equiv_assignments_cancel_cons; eauto 2.
}
{ rewrite <-EQ1, <-EQ2 in EQ, NEQ; clear EQ1 EQ2 NEQ.
apply non_equiv_assignments in EQ; assumption. }
{ rewrite <-EQ1, <-EQ2 in EQ, NEQ; clear EQ1 EQ2 NEQ.
apply non_equiv_assignments in EQ; assumption. }
{ rewrite <-EQ1, <-EQ2 in EQ, NEQ; clear EQ1 EQ2 α1 α2.
rename α1_tl into α1, α2_tl into α2.
apply neq_cons in NEQ.
specialize (IHvs _ _ EL1 EL2 NEQ).
apply IHvs; clear IHvs.
eapply equiv_assignments_cancel_cons; eauto 2.
}
}
}
Qed.
(* Any assignment that sets variables vs has an equivalen assignment
that belongs to the set with all assignments on variables vs. *)
Definition set_with_all_assignments_on (vs : variables) (αs : assignments) :=
set_with_all (equiv_assignments vs) (fun α => vs ⊆ vars_in α) αs.
Lemma all_assignments_in_all_assignments_on:
forall (vs : variables),
set_with_all_assignments_on vs (all_assignments_on vs).
Proof.
induction vs; intros α INCL.
{ exists []; split.
- intros v EL; inversion EL.
- left; auto. }
{ specialize (IHvs α); feed IHvs; auto.
{ intros v EL; apply INCL; right; auto. }
destruct IHvs as [β [EQU IN]].
destruct (mapsto_total α a) as [[[EL MAP]|[NEL2 NMAP]]|[EL MAP]].
{ exists ((a,true)::β); split.
{ intros v EL2; destruct EL2 as [EQ|EL2]; subst; intros b; split; intros EV.
- apply (mapsto_injective _ _ _ _ MAP) in EV; subst; constructor.
- inversion EV; subst; [ |exfalso]; auto.
- decide (a = v) as [EQ|NEQ]; [subst | ].
apply EQU in MAP; apply EQU in EV; auto.
apply (mapsto_injective _ _ _ _ MAP) in EV; subst; constructor.
constructor; auto; apply EQU; auto.
- decide (a = v) as [EQ|NEQ]; [subst | ].
+ inversion EV; subst; [ | exfalso]; auto.
+ inversion EV; subst; [exfalso | apply EQU]; auto.
}
{ simpl; apply in_app_iff; right.
apply in_map_iff; exists β; split; auto.
}
}
{ exfalso; apply NEL2; apply INCL; left; auto. }
{ exists ((a,false)::β); split.
{ intros v EL2; destruct EL2 as [EQ|EL2]; subst; intros b; split; intros EV.
- apply (mapsto_injective _ _ _ _ MAP) in EV; subst; constructor.
- inversion EV; subst; [ |exfalso]; auto.
- decide (a = v) as [EQ|NEQ]; [subst | ].
apply EQU in MAP; apply EQU in EV; auto.
apply (mapsto_injective _ _ _ _ MAP) in EV; subst; constructor.
constructor; auto; apply EQU; auto.
- decide (a = v) as [EQ|NEQ]; [subst | ].
+ inversion EV; subst; [ | exfalso]; auto.
+ inversion EV; subst; [exfalso | apply EQU]; auto.
}
{ simpl; apply in_app_iff; left.
apply in_map_iff; exists β; split; auto.
}
}
}
Qed.
Definition compute_formula (ϕ : formula) (α : assignment) (SET : sets_all_variables α ϕ):
{ b : bool | formula_eval ϕ α b }.
Proof.
induction ϕ.
- exists false; auto.
- exists true; auto.
- feed (SET v).
{ left; auto. }
destruct (mapsto_dec α v SET) as [M|M]; [exists true| exists false]; auto.
- destruct IHϕ as [b EV].
simpl in SET; assumption.
exists (negb b); constructor; rewrite Bool.negb_involutive; auto.
- apply inclusion_app in SET; destruct SET.
destruct IHϕ1 as [b1 EV1]; destruct IHϕ2 as [b2 EV2]; auto.
exists (andb b1 b2).
destruct b1, b2; simpl in *; try(constructor; auto; fail).
- simpl in SET; apply inclusion_app in SET; destruct SET.
destruct IHϕ1 as [b1 EV1]; destruct IHϕ2 as [b2 EV2]; auto.
exists (orb b1 b2).
destruct b1, b2; simpl in *; try(constructor; auto; fail).
Defined.
Definition formula_sat_filter (ϕ : formula) (α : assignment) : bool :=
match sets_all_variables_dec ϕ α with
| left _ SETS => let '(exist _ b _) := compute_formula ϕ α SETS in b
| right _ => false
end.
(* Now for a function ϕ, the algorithm
1) Generates the list of all assignments on ϕ's variables
2) Keeps assignment such that ℇ ϕ α ≡ true. *)
Definition algorithm1 (ϕ : formula) : { n : nat | #sat ϕ ≃ n }.
Proof.
set (vars := formula_vars ϕ).
assert(EX: { αs | list_of_all_sat_assignments ϕ αs }).
{ exists (filter (fun α => formula_sat_filter ϕ α) (all_assignments_on vars)).
split;[split | split].
{ apply nodup_filter.
destruct(list_of_all_assignments_dupfree vars).
- apply NoDup_nodup.
- assumption.
}
{ intros α1 α2 EL1 EL2 NEQ EQU.
apply filter_In in EL1; destruct EL1 as [EL1 SAT1].
apply filter_In in EL2; destruct EL2 as [EL2 SAT2].
apply equiv_assignments_nodup in EQU.
apply list_of_all_assignments_dupfree in EQU; try (apply NoDup_nodup || auto).
}
{ intros α EL.
apply filter_In in EL; destruct EL as [EL TR].
unfold formula_sat_filter in *; destruct (sets_all_variables_dec ϕ α) as [D|D]; [ | easy].
destruct (compute_formula ϕ α D) as [b EV]; subst b.
split; assumption.
}
{ intros α [SETS SAT].
assert(H := all_assignments_in_all_assignments_on vars α).
feed H; [eapply incl_tran; eauto; apply incl_nodup| ].
destruct H as [β [EQ EL]].
exists β; split.
- clear EL; intros ? EL b; split; intros EV.
all: apply EQ; auto; apply nodup_In; auto.
- apply filter_In; split; auto.
unfold formula_sat_filter; destruct (sets_all_variables_dec ϕ β) as [S|S].
+ apply equiv_assignments_nodup in EQ.
destruct (compute_formula ϕ β S) as [b EV].
apply formula_eval_assignment_transfer with (β := β) in SAT; auto.
eapply formula_eval_injective; eauto 2.
+ exfalso; apply S.
auto using assignment_in_all_assignments_on_sets_all_variables.
}
}
destruct EX as [αs AS]; exists (length αs); exists αs; split; auto.
Defined.
Section Tests.
Let x1 := [|V 1|].
Let x2 := [|V 2|].
Let x3 := [|V 3|].
Let x4 := [|V 4|].
Let x5 := [|V 5|].
Let or_n n := fold_left (fun ϕ x => ϕ ∨ [|V x|]) (range 1 n) F.
Let xor_n n := fold_left (fun ϕ x => ϕ ⊕ [|V x|]) (range 1 n) F.
(* Compute (proj1_sig (algorithm1 x1)). => 1 : nat *)
(* Compute (proj1_sig (algorithm1 (x1 ∨ x2 ∨ x3 ∨ x4 ∨ x5))). => 31 : nat *)
(* Compute (proj1_sig (algorithm1 (x1 ⊕ x2 ⊕ x3 ⊕ x4 ⊕ x5))). => 16 : nat *)
(* Compute (proj1_sig (algorithm1 (or_n 8))). => 255 : nat *)
(* It already takes a few seconds. *)
(* Compute (proj1_sig (algorithm1 (xor_n 8))). => 128 : nat *)
End Tests.
End Algorithm1.
(** * Algorithm 2: *)
(** With transformation ϕ = (ϕ[x ↦ T] ∧ x) ∨ (ϕ[x ↦ F] ∧ ¬x). *)
Section Algorithm2.
(* The main idea of the algorithm is the following:
#sat F = 0
#sat T = 1
#sat ϕ = #sat (x ∧ ϕ[x ↦ T] ∨ ¬x ∧ ϕ[x ↦ F])
= #sat (x ∧ ϕ[x ↦ T]) + #sat (¬x ∧ ϕ[x ↦ F])
= #sat (ϕ[x ↦ T]) + #sat (ϕ[x ↦ F]). *)
(* We start from "switch"-lemma which claims that
ϕ is equivalent to (ϕ[x ↦ T] ∧ x) ∨ (ϕ[x ↦ F] ∧ ¬x). *)
Section Switch.
(* For any formula ϕ and any assignments α which sets x to true
formulas ϕ and ϕ[x ↦ T] evaluates to the same value. *)
Lemma formula_eval_subst_T:
forall (ϕ : formula) (x : variable) (α : assignment) (b : bool),
x / α ↦ true ->
ℇ (ϕ) α ≡ b <-> ℇ (ϕ [x ↦ T]) α ≡ b.
Proof.
intros ϕ; induction ϕ; intros x α b M; split; intros EV.
all: try(inversion_clear EV; constructor; fail).
all: try(inversion_clear EV; simpl;
[ eapply ev_conj_t; [eapply IHϕ1|eapply IHϕ2]
| eapply ev_conj_fl; eapply IHϕ1
| eapply ev_conj_fr; eapply IHϕ2]; eauto).
all: try(inversion_clear EV; simpl;
[ eapply ev_disj_f; [eapply IHϕ1|eapply IHϕ2]
| eapply ev_disj_tl; eapply IHϕ1
| eapply ev_disj_tr; eapply IHϕ2]; eauto).
all: try(simpl; constructor; eapply IHϕ; [ | inversion_clear EV]; eauto).
- inversion_clear EV.
simpl in *; decide (x = v) as [EQ|NEQ];
[subst; apply (mapsto_injective _ _ _ _ H) in M; subst| ]; auto.
- simpl in *; decide (x = v) as [EQ|NEQ]; [subst; inversion_clear EV| ]; auto.
Qed.
(* Similarly for false. For any formula ϕ and any assignments α which
sets x to false formulas ϕ and ϕ[x ↦ F] evaluates to the same value. *)
Lemma formula_eval_subst_F:
forall (ϕ : formula) (x : variable) (α : assignment) (b : bool),
x / α ↦ false ->
ℇ (ϕ) α ≡ b <-> ℇ (ϕ [x ↦ F]) α ≡ b.
Proof.
intros ϕ; induction ϕ; intros x α b M; split; intros EV.
all: try(inversion_clear EV; constructor; fail).
all: try(inversion_clear EV; simpl;
[ eapply ev_conj_t; [eapply IHϕ1|eapply IHϕ2]
| eapply ev_conj_fl; eapply IHϕ1
| eapply ev_conj_fr; eapply IHϕ2]; eauto).
all: try(inversion_clear EV; simpl;
[ eapply ev_disj_f; [eapply IHϕ1|eapply IHϕ2]
| eapply ev_disj_tl; eapply IHϕ1
| eapply ev_disj_tr; eapply IHϕ2]; eauto).
all: try(simpl; constructor; eapply IHϕ; [ | inversion_clear EV]; eauto).
- inversion_clear EV.
simpl in *; decide (x = v) as [EQ|NEQ];
[subst; apply (mapsto_injective _ _ _ _ H) in M; subst| ]; auto.
- simpl in *; decide (x = v) as [EQ|NEQ]; [subst; inversion_clear EV| ]; auto.
Qed.
(* Proof by case analysis on [x / α ↦ b] and b. *)
Lemma switch:
forall (ϕ : formula) (x : variable) (α : assignment) (b : bool),
x el vars_in α ->
ℇ (ϕ) α ≡ b <-> ℇ ([|x|] ∧ ϕ[x ↦ T] ∨ ¬[|x|] ∧ ϕ[x ↦ F]) α ≡ b.
Proof.
intros ϕ ? ? ? SET.
destruct (mapsto_dec _ _ SET); destruct b; split; intros EV.
- apply ev_disj_tl; constructor; [ |apply formula_eval_subst_T]; auto.
- inversion_clear EV; inversion_clear H.
+ apply <-formula_eval_subst_T; eauto.
+ exfalso; clear H1.
inversion_clear H0; inversion_clear H.
apply (mapsto_injective _ _ _ _ m) in H0; inversion H0.
- eapply formula_eval_subst_T in EV; eauto; constructor;
[apply ev_conj_fr|apply ev_conj_fl]; auto.
- eapply formula_eval_subst_T; eauto.
inversion_clear EV; inversion_clear H0; inversion_clear H; try assumption.
+ inversion_clear H1; apply (formula_eval_injective _ _ _ _ H) in H0; inversion H0.
+ inversion_clear H0; apply (mapsto_injective _ _ _ _ H) in m; inversion m.
- apply ev_disj_tr; constructor; [ |apply formula_eval_subst_F]; auto.
- inversion_clear EV; inversion_clear H.
+ exfalso; clear H1.
inversion_clear H0.
apply (mapsto_injective _ _ _ _ m) in H; inversion H.
+ apply <-formula_eval_subst_F; eauto.
- eapply formula_eval_subst_F in EV; eauto.
- eapply formula_eval_subst_F; eauto.
inversion_clear EV; inversion_clear H0; inversion_clear H; try assumption.
+ inversion_clear H1; apply (formula_eval_injective _ _ _ _ H) in H0; inversion H0.
+ inversion_clear H1; inversion_clear H; apply (mapsto_injective _ _ _ _ H1) in m; inversion m.
Qed.
End Switch.
(* The algorithm proceeds by induction on formula size. *)
(* Any formula of size 0 is equivalent to either T or F. Moreover, we know that
T (of size 0) has one satisfying assignment and F has zero sat. assignments. *)
Section BaseCase.
Lemma formula_size_dec:
forall (ϕ : formula),
{formula_size ϕ = 0} + {formula_size ϕ > 0}.
Proof.
intros.
induction ϕ.
{ left; easy. }
{ left; easy. }
{ right; unfold formula_size; simpl; omega. }
{ destruct IHϕ as [IH|IH].
- left; assumption.
- right; assumption.
}
{ destruct IHϕ1 as [IH1|IH1].
- destruct IHϕ2 as [IH2|IH2].
+ left; unfold formula_size in *; simpl.
rewrite app_length, IH1, IH2. easy.
+ right; unfold formula_size in *; simpl.
rewrite app_length, IH1; easy.
- right; unfold formula_size in *; simpl.
rewrite app_length; omega.
}
{ destruct IHϕ1 as [IH1|IH1].
- destruct IHϕ2 as [IH2|IH2].
+ left; unfold formula_size in *; simpl.
rewrite app_length, IH1, IH2. easy.
+ right; unfold formula_size in *; simpl.
rewrite app_length, IH1; easy.
- right; unfold formula_size in *; simpl.
rewrite app_length; omega.
}
Defined.
Lemma zero_size_formula_constant_dec:
forall (ϕ : formula),
formula_size ϕ = 0 ->
{equivalent ϕ T} + {equivalent ϕ F}.
Proof.
intros ? SIZE.
induction ϕ.
{ right; intros ? ?; split; intros EV; auto. }
{ left; intros ? ?; split; intros EV; auto. }
{ exfalso; compute in SIZE; easy. }
{ rewrite formula_size_neg in SIZE.
feed IHϕ; auto.
destruct IHϕ as [IH|IH]; [right | left].
{ apply formula_equiv_neg_move.
apply formula_equiv_trans with T; auto.
apply formula_equiv_T_neg_F. }
{ apply formula_equiv_neg_move.
apply formula_equiv_trans with F; auto.
apply formula_equiv_sym, formula_equiv_neg_move, formula_equiv_T_neg_F. } }
{ rewrite formula_size_and in SIZE.
apply plus_is_O in SIZE.
destruct SIZE as [S1 S2].
feed IHϕ1; auto; feed IHϕ2; auto.
destruct IHϕ1 as [IH1|IH1].
- destruct IHϕ2 as [IH2|IH2].
+ left; apply formula_equiv_and_compose_T; auto.
+ right; clear IH1.
apply formula_equiv_trans with (ϕ2 ∧ ϕ1).
apply formula_equiv_and_comm. apply formula_equiv_and_compose_F; auto.
- right; clear IHϕ2.
apply formula_equiv_and_compose_F; auto.
}
{ rewrite formula_size_or in SIZE.
apply plus_is_O in SIZE.
destruct SIZE as [S1 S2].
feed IHϕ1; auto; feed IHϕ2; auto.
destruct IHϕ1 as [IH1|IH1].
- clear IHϕ2; left.
apply formula_equiv_or_compose_T; auto.
- destruct IHϕ2 as [IH2|IH2].
+ left. apply formula_equiv_trans with (ϕ2 ∨ ϕ1).
apply formula_equiv_or_comm. apply formula_equiv_or_compose_T; auto.
+ right. apply formula_equiv_or_compose_F; auto; apply fo_eq_11.
}
Defined.
Lemma number_or_satisfying_assignments_of_eqT:
forall (ϕ : formula),
equivalent ϕ T ->
#sat ϕ ≃ (Nat.pow 2 (length (formula_vars ϕ))).
Proof.
intros ? EQ.
exists (all_assignments_on (formula_vars ϕ)).
split; [split; [split | split] | ].
- apply list_of_all_assignments_dupfree.
apply NoDup_nodup.
- assert(H := list_of_all_assignments_dupfree
(formula_vars ϕ)).
feed H. apply NoDup_nodup. destruct H as [H1 H2].
intros ? ? EL1 EL2 NEQ EQU.
apply equiv_assignments_nodup in EQU.
apply H2 with (x1 := x1) (x2 := x2); auto.
- intros α EL; split.
auto using assignment_in_all_assignments_on_sets_all_variables.
apply EQ; constructor.
- intros α [SETS SAT].
assert(H := all_assignments_in_all_assignments_on (formula_vars ϕ) α).
feed H.
{ apply incl_tran with (leaves ϕ); try apply incl_nodup; auto. }
destruct H as [β [EQU EL]].
exists β; split; [apply equiv_assignments_nodup| ]; auto.
- rewrite size_of_list_of_all_assignments_on; auto.
Qed.
Corollary number_or_satisfying_assignments_of_T:
#sat T ≃ 1.
Proof.
apply number_or_satisfying_assignments_of_eqT, formula_equiv_refl.
Qed.
Lemma number_or_satisfying_assignments_of_eqF:
forall (ϕ : formula),
equivalent ϕ F ->
#sat ϕ ≃ 0.
Proof.
intros ? EQ.
exists []. split; [split; [split | split] | ]; auto.
- constructor.
- intros ? EL; destruct EL.
- intros α [_ SAT].
apply EQ in SAT.
inversion_clear SAT.
Qed.
Corollary number_or_satisfying_assignments_of_F:
#sat F ≃ 0.
Proof.
apply number_or_satisfying_assignments_of_eqF, formula_equiv_refl.
Qed.
End BaseCase.
(* For the induction step we assume that lists with satisfying
assignments are know for formulas ϕ[x ↦ T] and ϕ[x ↦ F]. *)
Section InductionStep.
(* Consider a formula ϕ. *)
Variable ϕ : formula.
(* And its leaf x. *)
Variable x : variable.
Hypothesis H_leaf : x el leaves ϕ.
(* Let αs1 and αs2 be lists of satisfying assignments for
formulas ϕ[x ↦ T] and ϕ[x ↦ F] respectively. *)
Variables αs1 αs2 : assignments.
Lemma app_sat_assignments_is_dupfree:
dupfree (leaves (ϕ [x ↦ T])) αs1 ->
dupfree (leaves (ϕ [x ↦ F])) αs2 ->
dupfree (leaves ϕ) (map (cons (x, true)) αs1 ++ map (cons (x, false)) αs2).
Proof.
intros [ND1 NE1] [ND2 NE2]; split.
{ apply nodup_app_of_map_cons; auto.
intros F; inversion_clear F.
}
{ intros α1 α2 EL1 EL2 EQ NEQ.
apply in_app_iff in EL1; apply in_app_iff in EL2.
destruct EL1 as [EL1|EL1], EL2 as [EL2|EL2].
{ apply in_map_iff in EL1; destruct EL1 as [β1 [EQ1 EL1]].
apply in_map_iff in EL2; destruct EL2 as [β2 [EQ2 EL2]]; subst α1 α2.
specialize (NE1 _ _ EL1 EL2).
feed NE1; [intros C; apply EQ; rewrite C; auto | ].
apply NE1; clear NE1.
apply equiv_assignments_cancel_subset with (vs_sub := leaves (ϕ [x ↦ T])) in NEQ;
auto using leaves_subset_subst_T, leaves_nel_subst_T.
}
{ apply in_map_iff in EL1; apply in_map_iff in EL2.
destruct EL1 as [α1_tl [EQ1 _]], EL2 as [α2_tl [EQ2 _]]; subst α1 α2.
specialize (NEQ x H_leaf true); destruct NEQ as [NEQ _]; feed NEQ; auto.
inversion_clear NEQ; auto.
}
{ apply in_map_iff in EL1; apply in_map_iff in EL2.
destruct EL1 as [α1_tl [EQ1 _]], EL2 as [α2_tl [EQ2 _]]; subst α1 α2.
specialize (NEQ x H_leaf true); destruct NEQ as [_ NEQ]; feed NEQ; auto.
inversion_clear NEQ; auto.
}
{ apply in_map_iff in EL1; destruct EL1 as [β1 [EQ1 EL1]].
apply in_map_iff in EL2; destruct EL2 as [β2 [EQ2 EL2]]; subst α1 α2.
specialize (NE2 _ _ EL1 EL2).
feed NE2; [intros C; apply EQ; rewrite C; auto | ].
apply NE2; clear NE2.
apply equiv_assignments_cancel_subset with (vs_sub := leaves (ϕ [x ↦ F])) in NEQ;
auto using leaves_subset_subst_F, leaves_nel_subst_F.
}
}
Qed.
Lemma app_sat_assignments_is_set_with_sat_assignments:
set_with_sat_assignments (ϕ[x ↦ T]) αs1 ->
set_with_sat_assignments (ϕ[x ↦ F]) αs2 ->
set_with_sat_assignments
ϕ (map (cons (x, true)) αs1 ++ map (cons(x, false)) αs2).
Proof.
intros SAT1 SAT2; intros α ELt; split.
{ apply in_app_iff in ELt; destruct ELt as [EL|EL]; apply in_map_iff in EL;
destruct EL as [α_tl [EQ EL]]; subst α.
- intros v IN.
decide (x = v) as [EQ|NEQ]; subst.
+ left; auto.
+ specialize (SAT1 α_tl EL); destruct SAT1 as [SET1 _].
right; apply SET1, leaves_el_neq_subst_T; auto.
- intros v IN.
decide (x = v) as [EQ|NEQ]; subst.
+ left; auto.
+ specialize (SAT2 α_tl EL); destruct SAT2 as [SET2 _].
right; apply SET2, leaves_el_neq_subst_F; auto.
}
apply switch with x.
{ apply in_app_iff in ELt; destruct ELt as [EL|EL]; apply in_map_iff in EL;
destruct EL as [α_tl [EQ EL]]; subst α; simpl; left; auto. }
apply in_app_or in ELt; destruct ELt as [EL|EL].
{ apply ev_disj_tl, ev_conj_t.
{ apply in_map_iff in EL.
destruct EL as [mα [EQ1 MEM1]]; subst α; auto.
}
{ apply in_map_iff in EL.
destruct EL as [mα [EQ MEM]]; subst α.
apply formula_eval_nel_cons, SAT1; auto using leaves_nel_subst_T; auto.
}
}
{ apply ev_disj_tr, ev_conj_t.
{ apply in_map_iff in EL.
destruct EL as [mα [EQ MEM]]; subst α; auto.
}
{ apply in_map_iff in EL.
destruct EL as [mα [EQ MEM]]; subst α.
apply formula_eval_nel_cons, SAT2; auto using leaves_nel_subst_F; auto.
}
}
Qed.
Lemma app_sat_assignments_is_set_with_all_sat_assignments:
set_with_all_sat_assignments (ϕ [x ↦ T]) αs1 ->
set_with_all_sat_assignments (ϕ [x ↦ F]) αs2 ->
set_with_all_sat_assignments
ϕ (map (cons (x, true)) αs1 ++ map (cons (x, false)) αs2).
Proof.
intros SET1 SET2.
intros α [SETS SAT].
apply (switch _ x _ _ (SETS x H_leaf)) in SAT.
inversion_clear SAT; inversion_clear H.
{ specialize (SET1 α); feed SET1.
{ split; [apply sets_all_variables_subst_T| ]; auto. }
destruct SET1 as [β [EQ EL]].
inversion_clear H0.
exists ((x,true)::β); split.
{ intros v ELl b.
decide (v = x) as [E|NEQ]; [subst | ]; split; intros EV.
- apply (mapsto_injective _ _ _ _ H) in EV; subst; constructor.
- inversion_clear EV; [ | exfalso]; auto.
- constructor; auto; apply EQ; auto using leaves_el_neq_subst_T.
- inversion_clear EV; auto; apply EQ; auto using leaves_el_neq_subst_T.
}
{ apply in_app_iff; left.
apply in_map_iff; exists β; easy.
}
}
{ specialize (SET2 α); feed SET2.
{ split; [apply sets_all_variables_subst_F| ]; auto. }
destruct SET2 as [β [EQ EL]].
inversion_clear H0; inversion_clear H; simpl in H0.
exists ((x,false)::β); split.
{ intros v ELl b.
decide (v = x) as [E|NEQ]; [subst | ]; split; intros EV.
- apply (mapsto_injective _ _ _ _ H0) in EV; subst; constructor.
- inversion_clear EV; [ | exfalso]; auto.
- constructor; auto; apply EQ; auto using leaves_el_neq_subst_F.
- inversion_clear EV; auto; apply EQ; auto using leaves_el_neq_subst_F.
}
{ apply in_app_iff; right.
apply in_map_iff; exists β; easy.
}
}
Qed.
Lemma app_sat_assignments_sum_length:
forall (nl nr : nat),
length αs1 = nl ->
length αs2 = nr ->
length (map (cons (x, true)) αs1 ++ map (cons (x, false)) αs2) = nl + nr.
Proof.
intros nl nr LEN1 LEN2.
rewrite app_length, map_length, map_length, <- LEN1, <- LEN2; auto.
Qed.
End InductionStep.
Definition algorithm2 (ϕ : formula) : { n : nat | #sat ϕ ≃ n }.
Proof.
generalize dependent ϕ.
apply size_recursion with formula_size; intros ϕ IHϕ.
destruct (formula_size_dec ϕ) as [Zero|Pos].
{ destruct (zero_size_formula_constant_dec ϕ Zero) as [Tr|Fl].
- exists 1.
assert(EQ := nodup_length_le _ (leaves ϕ)); unfold formula_size in Zero;
rewrite Zero in EQ; rewrite Nat.le_0_r in EQ.
assert(One := number_or_satisfying_assignments_of_eqT ϕ Tr); unfold formula_vars in One;
rewrite EQ in One; simpl in One.
assumption.
- exists 0; auto using number_or_satisfying_assignments_of_eqF. }
{ assert (V := get_var _ Pos).
destruct V as [x IN]; clear Pos.
assert (IH1 := IHϕ (ϕ[x ↦ T])); assert(IH2 := IHϕ (ϕ[x ↦ F])); clear IHϕ.
specialize (IH1 (formula_size_subst_T_lt _ _ IN));
specialize (IH2 (formula_size_subst_F_lt _ _ IN)).
destruct IH1 as [nl EQ1], IH2 as [nr EQ2].
exists (nl + nr).
destruct EQ1 as [αs1 [LAA1 LEN1]], EQ2 as [αs2 [LAA2 LEN2]].
exists (map (fun α => (x, true)::α) αs1 ++ map (fun α => (x,false)::α) αs2).
destruct LAA1 as [ND1 [SAT1 SET1]], LAA2 as [ND2 [SAT2 SET2]].
split; [split; [ | split] | ];
auto using app_sat_assignments_is_dupfree,
app_sat_assignments_is_set_with_sat_assignments,
app_sat_assignments_is_set_with_all_sat_assignments,
app_sat_assignments_sum_length.
}
Defined.
Section Tests.
Let or_n n := fold_left (fun ϕ x => ϕ ∨ [|V x|]) (range 1 n) F.
Let xor_n n := fold_left (fun ϕ x => ϕ ⊕ [|V x|]) (range 1 n) F.
(* Compute (proj1_sig (algorithm1 (or_n 5))). => 31 : nat *)
(* Compute (proj1_sig (algorithm1 (or_n 8))). => 255 : nat *)
(* Compute (proj1_sig (algorithm1 (or_n 10))). => 1023 : nat *)
(* Compute (proj1_sig (algorithm1 (or_n 15))). => 32767 : nat *)
(* Compute (proj1_sig (algorithm1 (or_n 16))). => Stack overflow. *)
(* Compute (proj1_sig (algorithm1 (xor_n 5))). => 16 : nat *)
(* Compute (proj1_sig (algorithm1 (xor_n 8))). => 128 : nat *)
End Tests.
End Algorithm2.
(** * Bonus 1: A (failed) attempt to come up with a third algorithm. *)
(* Algorithm
1) Transform ϕ to DNF form
2) Map each monomial into a certificate1
3) Make these certificates disjoint
(i.e. they set at least one variable to different values)
4) Calculate the number of sat. assignments. *)
Section Algorithm3.
Section Literal.
Inductive literal :=
| Positive: variable -> literal
| Negative: variable -> literal.
Inductive literal_eval: literal -> assignment -> bool -> Prop :=
| lit_ev_pos: forall (v : variable) (α : assignment) (b : bool),
(v / α ↦ b) -> literal_eval (Positive v) α b
| lit_ev_neg: forall (v : variable) (α : assignment) (b : bool),
(v / α ↦ (negb b)) -> literal_eval (Negative v) α b.
Lemma literal_eval_injective:
forall (α : assignment) (l : literal) (b1 b2 : bool),
literal_eval l α b1 ->
literal_eval l α b2 ->
b1 = b2.
Proof.
intros ? ? ? ? M1 M2.
destruct b1, b2; auto; exfalso.
all: inversion M1; subst; inversion M2; subst.
all: eapply mapsto_injective_contr; eauto.
Qed.
Corollary literal_eval_injective_contr:
forall (α : assignment) (l : literal),
literal_eval l α true ->
literal_eval l α false ->
False.
Proof.
intros ? ? EV1 EV2; assert (F := literal_eval_injective _ _ _ _ EV1 EV2); easy.
Qed.
End Literal.
Hint Constructors literal_eval.
Section Monomial.
Definition monomial := list literal.
Inductive monomial_eval: monomial -> assignment -> bool -> Prop :=
| mon_ev_true: forall (m : monomial) (α : assignment),
(forall l, l el m -> literal_eval l α true) ->
monomial_eval m α true
| mon_ev_false: forall (m : monomial) (α : assignment),
(exists l, l el m /\ literal_eval l α false) ->
monomial_eval m α false.
Definition monomial_sat_assignment (m : monomial) (α : assignment) :=
monomial_eval m α true.
Definition monomial_satisfiable (m : monomial) :=
exists (α : assignment), monomial_sat_assignment m α.
Definition monomial_unsat_assignment (m : monomial) (α : assignment) :=
monomial_eval m α false.
Definition monomial_unsatisfiable (m : monomial) :=
forall (α : assignment), monomial_unsat_assignment m α.
Lemma literal_eval_total:
forall (α : assignment) (m : monomial),
(forall l, l el m -> literal_eval l α true) \/
((exists l, l el m /\ forall b, ~ literal_eval l α b)
/\ (forall l, l el m -> (exists b, literal_eval l α b) -> literal_eval l α true)) \/
(exists l, l el m /\ literal_eval l α false).
Proof.
clear; intros; induction m.
left; intros l EL; inversion EL.
destruct IHm as [IH|[IH|IH]].
{ destruct a; destruct (mapsto_total α v) as [[[V H]|[V H]]|[V H]].
- left; intros l EL; destruct EL as [EQ|IN]; subst; auto.
- right; left; split.
+ exists (Positive v); split; [left| ]; auto.
intros b EV; inversion_clear EV.
apply nel_mapsto in H0; auto.
+ intros ? [EQ|EL] [b EV]; subst; apply IH; auto.
inversion_clear EV; specialize (H _ H0); destruct H.
- right; right; exists (Positive v); split; [left| ]; auto.
- right; right; exists (Negative v); split; [left| ]; auto.
- right; left; split.
+ exists (Negative v); split; [left| ]; auto.
intros b EV; inversion_clear EV.
apply nel_mapsto in H0; auto.
+ intros ? [EQ|EL] [b EV]; subst; apply IH; auto.
inversion_clear EV; specialize (H _ H0); destruct H.
- left; intros l EL; destruct EL as [EQ|IN]; subst; auto.
}
{ destruct IH as [[l [EL NE]] ALL], a, (mapsto_total α v) as [[[V H]|[V H]]|[V H]]; right.
- left; split.
+ exists l; split; [right | ]; auto.
+ intros l2 [EQ|EL2] [b EV]; subst; [constructor|apply ALL]; eauto.
- left; split.
+ exists l; split; [right | ]; auto.
+ intros l2 [EQ|EL2] [b EV]; subst.
exfalso; inversion_clear EV; eapply H; eauto.
apply ALL; eauto.
- right.
exists (Positive v); split; [left| ]; auto.
- right.
exists (Negative v); split; [left| ]; auto.
- left; split.
+ exists l; split; [right | ]; auto.
+ intros l2 [EQ|EL2] [b EV]; subst.
exfalso; inversion_clear EV; eapply H; eauto.
apply ALL; eauto.
- left; split.
+ exists l; split; [right | ]; auto.
+ intros l2 [EQ|EL2] [b EV]; subst; [constructor|apply ALL]; eauto.
}
{ destruct IH as [l [EL NE]].
right; right.
exists l; split; [right | ]; auto.
}
Qed.
End Monomial.
Section DNF.
Definition dnf := list monomial.
Inductive dnf_eval: dnf -> assignment -> bool -> Prop :=
| dnf_ev_true: forall (d : dnf) (α : assignment),
(exists m, m el d /\ monomial_eval m α true) ->
dnf_eval d α true
| dnf_ev_false: forall (d : dnf) (α : assignment),
(forall m, m el d -> monomial_eval m α false) ->
dnf_eval d α false.
Definition dnf_representation (ϕ : formula) (ψ : dnf) :=
forall (α : assignment) (b : bool),
formula_eval ϕ α b <-> dnf_eval ψ α b.
Definition equivalent_dnf (ψ1 ψ2 : dnf) :=
forall (α : assignment) (b : bool),
dnf_eval ψ1 α b <-> dnf_eval ψ2 α b.
Lemma dnf_representation_formula_transfer:
forall (ϕ1 ϕ2 : formula) (ψ : dnf),
equivalent ϕ1 ϕ2 ->
dnf_representation ϕ2 ψ ->
dnf_representation ϕ1 ψ.
Proof.
intros ? ? ? EQU DNF1.
intros ? b; split; intros EV.
apply DNF1, EQU; assumption.
apply EQU, DNF1; assumption.
Qed.
Corollary dnf_representation_sigma_formula_transfer:
forall (ϕ1 ϕ2 : formula),
equivalent ϕ1 ϕ2 ->
{ψ : dnf | dnf_representation ϕ1 ψ} ->
{ψ : dnf | dnf_representation ϕ2 ψ}.
Proof.
intros ? ? EQ REP.
destruct REP as [ψ REP].
exists ψ; apply dnf_representation_formula_transfer with ϕ1; auto.
apply formula_equiv_sym; assumption.
Qed.
Lemma monomial_sat_total:
forall (α : assignment) (ψ : dnf),
(forall m, m el ψ -> monomial_unsat_assignment m α) \/
(exists m, m el ψ /\ forall b, ~ monomial_eval m α b) \/
(exists m, m el ψ /\ monomial_sat_assignment m α).
Proof.
intros.
induction ψ.
- left; intros; inversion_clear H.
- destruct IHψ as [IH|[IH|IH]].
+ destruct (literal_eval_total α a) as [H|[H|H]].
* right; right.
exists a; split; [left|constructor]; auto.
* right; left; destruct H as [[l [EL NO]] ALL].
exists a; split; [left| ]; auto; intros [ | ] MON.
apply NO with (b := true); inversion_clear MON; auto.
inversion_clear MON; destruct H as [l2 [EL2 NO2]].
specialize (ALL l2 EL2 (@ex_intro _ (literal_eval l2 α) false NO2)).
eapply literal_eval_injective_contr; eauto.
* left.
destruct H as [l [EL ALL]].
intros m [EQ|EL2]; subst.
constructor; exists l; split; auto.
apply IH; auto.
+ right; left.
destruct IH as [m [EL ALL]].
exists m; split; [right| ]; auto.
+ right; right.
destruct IH as [m [EL ALL]].
exists m; split; [right| ]; auto.
Qed.
End DNF.
Section FormulaToDNF.
Fixpoint bottom_negations (ϕ : formula) : Prop :=
match ϕ with
| T | F | [|_|] | ¬ [|_|]=> True
| ϕl ∧ ϕr => bottom_negations ϕl /\ bottom_negations ϕr
| ϕl ∨ ϕr => bottom_negations ϕl /\ bottom_negations ϕr
| ¬ _ => False
end.
(* By repetitive application of DeMorgan's laws, one
can move all negations to the bottom of a formula. *)
Definition move_negations (ϕ : formula):
{neg_ϕ : formula | equivalent ϕ neg_ϕ
/\ bottom_negations neg_ϕ }.
Proof.
generalize dependent ϕ.
apply size_recursion with number_of_nodes; intros ϕ IH.
destruct ϕ.
{ (* move_negations F := F. *)
exists F; split.
- apply formula_equiv_refl.
- constructor.
}
{ (* move_negations T := T. *)
exists T; split.
- apply formula_equiv_refl.
- constructor.
}
{ (* move_negations [|v|] := [|v|]. *)
exists [|v|]; split.
- apply formula_equiv_refl.
- constructor.
}
{ destruct ϕ.
{ (* move_negations (¬F) := T. *)
exists T; split.
- apply formula_equiv_sym;
apply formula_equiv_T_neg_F.
- constructor.
}
{ (* move_negations (¬T) := F. *)
exists F; split.
- apply formula_equiv_neg_move;
apply formula_equiv_T_neg_F.
- constructor.
}
{ (* move_negations (¬[|v|]) := ¬ [|v|]. *)
exists (¬ [|v|]); split.
- apply formula_equiv_refl.
- constructor.
}
{ (* move_negations (¬ ¬ ϕ) := move_negations ϕ. *)
assert (IH1 := IH ϕ); feed IH1; [simpl; omega| clear IH].
destruct IH1 as [neg_ϕ [EQ LIT]].
exists neg_ϕ; split.
- apply formula_equiv_neg_move.
apply ->formula_equiv_neg_compose; assumption.
- assumption.
}
{ (* move_negations (¬(ϕl ∧ ϕr)) := move_negations ϕl ∨ move_negations ϕr. *)
assert (IH1 := IH (¬ ϕ1)); feed IH1; [simpl; omega| ].
assert (IH2 := IH (¬ ϕ2)); feed IH2; [simpl; omega| clear IH].
destruct IH1 as [neg_ϕ1 [EQ1 BOT1]], IH2 as [neg_ϕ2 [EQ2 BOT2]].
exists (neg_ϕ1 ∨ neg_ϕ2); split.
- apply formula_equiv_neg_move.
apply formula_equiv_trans with (¬(¬ϕ1 ∨ ¬ϕ2)).
apply formula_equiv_demorgan_and.
apply ->formula_equiv_neg_compose; apply formula_equiv_or_compose; auto.
- split; assumption.
}
{ (* move_negations (¬(ϕl ∨ ϕr)) := move_negations ϕl ∧ move_negations ϕr. *)
assert (IH1 := IH (¬ ϕ1)); feed IH1; [simpl; omega| ].
assert (IH2 := IH (¬ ϕ2)); feed IH2; [simpl; omega| ].
destruct IH1 as [neg_ϕ1 [EQ1 BOT1]], IH2 as [neg_ϕ2 [EQ2 BOT2]].
exists (neg_ϕ1 ∧ neg_ϕ2); split.
- apply formula_equiv_neg_move.
apply formula_equiv_trans with (¬(¬ϕ1 ∧ ¬ϕ2)).
apply formula_equiv_demorgan_or.
apply ->formula_equiv_neg_compose; apply formula_equiv_and_compose; auto.
- split; assumption.
}
}
{ (* move_negations (ϕl ∧ ϕr) := move_negations ϕl ∧ move_negations ϕr. *)
assert (IH1 := IH ϕ1); feed IH1; [simpl; omega| ].
assert (IH2 := IH ϕ2); feed IH2; [simpl; omega| ].
destruct IH1 as [neg_ϕ1 [EQ1 BOT1]], IH2 as [neg_ϕ2 [EQ2 BOT2]].
exists (neg_ϕ1 ∧ neg_ϕ2); split.
- apply formula_equiv_and_compose; assumption.
- split; assumption.
}
{ (* move_negations (ϕl ∨ ϕr) := move_negations ϕl ∨ move_negations ϕr. *)
assert (IH1 := IH ϕ1); feed IH1; [simpl; omega| ].
assert (IH2 := IH ϕ2); feed IH2; [simpl; omega| ].
destruct IH1 as [neg_ϕ1 [EQ1 BOT1]], IH2 as [neg_ϕ2 [EQ2 BOT2]].
exists (neg_ϕ1 ∨ neg_ϕ2); split.
- apply formula_equiv_or_compose; auto.
- split; assumption.
}
Qed.
(* Next we inductively transform a formula into its DNF representation. *)
Lemma dnf_representation_of_T:
dnf_representation T [[]].