Skip to content

Commit

Permalink
update dependencies
Browse files Browse the repository at this point in the history
  • Loading branch information
@olaure01
olaure01 committed Jan 23, 2019
1 parent 2f0c001 commit 51df5e9
Show file tree
Hide file tree
Showing 4 changed files with 25 additions and 23 deletions.
33 changes: 17 additions & 16 deletions yalla/Makefile
View file
Expand Up @@ -50,38 +50,39 @@ cutelim: ollibs $(VFILES:.v=.vo)
include $(OLLIBSDIR)/ollibs.mk

basic_misc.vo: basic_misc.v $(OLLIBSDIR)/Permutation_Type_solve.vo $(OLLIBSDIR)/genperm_Type.vo
yalla_ax.vo: yalla_ax.v $(OLLIBSDIR)/Injective.vo

formulas.vo: formulas.v $(OLLIBSDIR)/Injective.vo $(OLLIBSDIR)/Bool_more.vo yalla_ax.vo
fmformulas.vo: fmformulas.v $(OLLIBSDIR)/Injective.vo $(OLLIBSDIR)/nattree.vo $(OLLIBSDIR)/fmsetlist_Type.vo formulas.vo
ll_fragments.vo: ll_fragments.v $(OLLIBSDIR)/Bool_more.vo $(OLLIBSDIR)/List_more.vo $(OLLIBSDIR)/List_Type_more.vo $(OLLIBSDIR)/Permutation_Type_more.vo $(OLLIBSDIR)/Permutation_Type_solve.vo $(OLLIBSDIR)/genperm_Type.vo ll_prop.vo subs.vo
ll_def.vo: ll_def.v $(OLLIBSDIR)/Bool_more.vo $(OLLIBSDIR)/List_more.vo $(OLLIBSDIR)/List_Type_more.vo $(OLLIBSDIR)/Permutation_Type_more.vo $(OLLIBSDIR)/CyclicPerm_Type.vo $(OLLIBSDIR)/Permutation_Type_solve.vo $(OLLIBSDIR)/CPermutation_Type_solve.vo $(OLLIBSDIR)/genperm_Type.vo basic_misc.vo formulas.vo
subs.vo: subs.v $(OLLIBSDIR)/List_more.vo $(OLLIBSDIR)/Permutation_Type.vo $(OLLIBSDIR)/genperm_Type.vo ll_def.vo
ll_cut.vo: ll_cut.v $(OLLIBSDIR)/Injective.vo $(OLLIBSDIR)/List_more.vo $(OLLIBSDIR)/List_Type_more.vo $(OLLIBSDIR)/Permutation_Type_more.vo $(OLLIBSDIR)/genperm_Type.vo $(OLLIBSDIR)/flat_map_Type_more.vo $(OLLIBSDIR)/wf_nat_more.vo ll_def.vo
ll_prop.vo: ll_prop.v $(OLLIBSDIR)/Bool_more.vo $(OLLIBSDIR)/List_more.vo $(OLLIBSDIR)/Permutation_Type_more.vo $(OLLIBSDIR)/CyclicPerm_Type.vo $(OLLIBSDIR)/genperm_Type.vo ll_cut.vo
ll_fragments.vo: ll_fragments.v $(OLLIBSDIR)/Bool_more.vo $(OLLIBSDIR)/List_more.vo $(OLLIBSDIR)/List_Type_more.vo $(OLLIBSDIR)/Permutation_Type_more.vo $(OLLIBSDIR)/Permutation_Type_solve.vo $(OLLIBSDIR)/genperm_Type.vo ll_prop.vo subs.vo

iformulas.vo: iformulas.v $(OLLIBSDIR)/Bool_more.vo yalla_ax.vo
fmiformulas.vo: fmiformulas.v $(OLLIBSDIR)/Injective.vo $(OLLIBSDIR)/nattree.vo $(OLLIBSDIR)/fmsetlist_Type.vo iformulas.vo
ill_def.vo: ill_def.v $(OLLIBSDIR)/Bool_more.vo $(OLLIBSDIR)/List_more.vo $(OLLIBSDIR)/List_Type_more.vo $(OLLIBSDIR)/Permutation_Type_more.vo $(OLLIBSDIR)/genperm_Type.vo basic_misc.vo iformulas.vo
isubs.vo: isubs.v $(OLLIBSDIR)/List_more.vo $(OLLIBSDIR)/Permutation_Type.vo $(OLLIBSDIR)/genperm_Type.vo ill_def.vo
ill_cut.vo: ill_cut.v $(OLLIBSDIR)/Injective.vo $(OLLIBSDIR)/List_more.vo $(OLLIBSDIR)/List_Type_more.vo $(OLLIBSDIR)/Permutation_Type_more.vo $(OLLIBSDIR)/genperm_Type.vo $(OLLIBSDIR)/flat_map_Type_more.vo $(OLLIBSDIR)/wf_nat_more.vo ill_def.vo
ill_prop.vo: ill_prop.v $(OLLIBSDIR)/Bool_more.vo $(OLLIBSDIR)/List_more.vo $(OLLIBSDIR)/Permutation_Type_more.vo $(OLLIBSDIR)/genperm_Type.vo ill_cut.vo
ill_vs_ll.vo: ill_vs_ll.v $(OLLIBSDIR)/Injective.vo $(OLLIBSDIR)/List_more.vo $(OLLIBSDIR)/List_Type_more.vo $(OLLIBSDIR)/Permutation_Type_more.vo $(OLLIBSDIR)/Permutation_Type_solve.vo $(OLLIBSDIR)/genperm_Type.vo ll_fragments.vo ill_prop.vo
subs.vo: subs.v $(OLLIBSDIR)/List_more.vo $(OLLIBSDIR)/genperm.vo ll_def.vo
isubs.vo: isubs.v $(OLLIBSDIR)/List_more.vo $(OLLIBSDIR)/genperm.vo ill_def.vo

ll_smp.vo: ll_smp.v $(OLLIBSDIR)/Injective.vo $(OLLIBSDIR)/List_Type_more.vo $(OLLIBSDIR)/Permutation_Type_more.vo $(OLLIBSDIR)/Permutation_Type_solve.vo ll_cut.vo ll_fragments.vo $(MICROYALLADIR)/ll.vo
ill_smp.vo: ill_smp.v $(OLLIBSDIR)/Injective.vo $(OLLIBSDIR)/List_Type_more.vo $(OLLIBSDIR)/Permutation_Type_more.vo $(OLLIBSDIR)/Permutation_Type_solve.vo ill_cut.vo $(MICROYALLADIR)/ill.vo
mell2.vo: mell2.v $(OLLIBSDIR)/Injective.vo $(OLLIBSDIR)/List_Type_more.vo $(OLLIBSDIR)/Permutation_Type_more.vo $(OLLIBSDIR)/Permutation_Type_solve.vo ll_cut.vo
mell_Prop.vo: mell_Prop.v $(OLLIBSDIR)/Injective.vo $(OLLIBSDIR)/List_more.vo $(OLLIBSDIR)/Permutation_more.vo $(OLLIBSDIR)/Permutation_solve.vo ll_cut.vo
lambek.vo: lambek.v $(OLLIBSDIR)/Injective.vo $(OLLIBSDIR)/List_more.vo $(OLLIBSDIR)/List_Type_more.vo ill_cut.vo
mell_mset.vo : mell_mset.v $(OLLIBSDIR)/Injective.vo $(OLLIBSDIR)/nattree.vo $(OLLIBSDIR)/List_more.vo $(OLLIBSDIR)/Permutation_more.vo $(OLLIBSDIR)/fmsetlist.vo ll_cut.vo fmformulas.vo
mell_msetoid.vo : mell_msetoid.v $(OLLIBSDIR)/Injective.vo $(OLLIBSDIR)/fmsetoidlist.vo $(OLLIBSDIR)/List_more.vo $(OLLIBSDIR)/Permutation_more.vo ll_cut.vo
llpol.vo: llpol.v $(OLLIBSDIR)/Injective.vo $(OLLIBSDIR)/List_more.vo $(OLLIBSDIR)/List_Type_more.vo $(OLLIBSDIR)/Permutation_Type.vo $(OLLIBSDIR)/Permutation_Type_more.vo $(OLLIBSDIR)/Permutation_Type_solve.vo ll_cut.vo
llfoc.vo: llfoc.v $(OLLIBSDIR)/List_more.vo $(OLLIBSDIR)/Permutation_more.vo $(OLLIBSDIR)/genperm.vo ll_fragments.vo
tl.vo: tl.v $(OLLIBSDIR)/Injective.vo $(OLLIBSDIR)/Bool_more.vo $(OLLIBSDIR)/List_more.vo $(OLLIBSDIR)/List_Type_more.vo $(OLLIBSDIR)/Permutation_Type_more.vo $(OLLIBSDIR)/genperm.vo ill_vs_ll.vo ll_def.vo

yalla_ax.vo: $(OLLIBSDIR)/Injective.vo yalla_ax.v

llfoc.vo: llfoc.v $(OLLIBSDIR)/List_more.vo $(OLLIBSDIR)/List_Type.vo $(OLLIBSDIR)/List_Type_more.vo $(OLLIBSDIR)/Permutation_Type_more.vo $(OLLIBSDIR)/Permutation_Type_solve.vo $(OLLIBSDIR)/genperm_Type.vo ll_fragments.vo
bbb.vo: bbb.v $(OLLIBSDIR)/List_more.vo $(OLLIBSDIR)/List_Type_more.vo $(OLLIBSDIR)/Permutation_Type_more.vo $(OLLIBSDIR)/Permutation_Type_solve.vo $(OLLIBSDIR)/genperm_Type.vo ll_fragments.vo
tl.vo: tl.v $(OLLIBSDIR)/Injective.vo $(OLLIBSDIR)/Bool_more.vo $(OLLIBSDIR)/List_more.vo $(OLLIBSDIR)/List_Type_more.vo $(OLLIBSDIR)/Permutation_Type_more.vo $(OLLIBSDIR)/genperm_Type.vo ill_vs_ll.vo ll_def.vo
nn_def.vo: nn_def.v $(OLLIBSDIR)/Injective.vo $(OLLIBSDIR)/List_more.vo $(OLLIBSDIR)/Permutation_Type.vo $(OLLIBSDIR)/genperm_Type.vo subs.vo isubs.vo ill_vs_ll.vo
nn_prop.vo: nn_prop.v $(OLLIBSDIR)/List_more.vo $(OLLIBSDIR)/List_Type_more.vo $(OLLIBSDIR)/Permutation_Type.vo $(OLLIBSDIR)/genperm_Type.vo subs.vo ll_fragments.vo nn_def.vo bbb.vo
nn_foc.vo: nn_foc.v $(OLLIBSDIR)/Injective.vo $(OLLIBSDIR)/List_more.vo $(OLLIBSDIR)/List_Type_more.vo $(OLLIBSDIR)/Permutation_Type_more.vo $(OLLIBSDIR)/Permutation_Type_solve.vo $(OLLIBSDIR)/genperm_Type.vo ll_fragments.vo llfoc.vo tl.vo nn_prop.vo

ll_smp.vo: ll_smp.v $(OLLIBSDIR)/Injective.vo $(OLLIBSDIR)/List_Type_more.vo $(OLLIBSDIR)/Permutation_Type_more.vo $(OLLIBSDIR)/Permutation_Type_solve.vo ll_fragments.vo $(MICROYALLADIR)/ll.vo
ill_smp.vo: ill_smp.v $(OLLIBSDIR)/Injective.vo $(OLLIBSDIR)/List_Type_more.vo $(OLLIBSDIR)/Permutation_Type_more.vo $(OLLIBSDIR)/Permutation_Type_solve.vo ill_cut.vo $(MICROYALLADIR)/ill.vo
mell2.vo: mell2.v $(OLLIBSDIR)/Injective.vo $(OLLIBSDIR)/List_Type_more.vo $(OLLIBSDIR)/Permutation_Type_more.vo $(OLLIBSDIR)/Permutation_Type_solve.vo ll_cut.vo
mell_Prop.vo: mell_Prop.v $(OLLIBSDIR)/Injective.vo $(OLLIBSDIR)/List_more.vo $(OLLIBSDIR)/Permutation_more.vo $(OLLIBSDIR)/Permutation_solve.vo $(OLLIBSDIR)/Permutation_Type_more.vo $(OLLIBSDIR)/Permutation_Type_solve.vo ll_cut.vo
mell_mset.vo : mell_mset.v $(OLLIBSDIR)/Injective.vo $(OLLIBSDIR)/nattree.vo $(OLLIBSDIR)/fmsetlist_Type.vo $(OLLIBSDIR)/List_more.vo $(OLLIBSDIR)/List_Type_more.vo $(OLLIBSDIR)/Permutation_more.vo $(OLLIBSDIR)/Permutation_Type_more.vo ll_cut.vo fmformulas.vo
mell_msetoid.vo : mell_msetoid.v $(OLLIBSDIR)/Injective.vo $(OLLIBSDIR)/fmsetoidlist_Type.vo $(OLLIBSDIR)/List_more.vo $(OLLIBSDIR)/Permutation_Type_more.vo ll_cut.vo
llpol.vo: llpol.v $(OLLIBSDIR)/Injective.vo $(OLLIBSDIR)/List_more.vo $(OLLIBSDIR)/List_Type_more.vo $(OLLIBSDIR)/Permutation_Type.vo $(OLLIBSDIR)/Permutation_Type_more.vo $(OLLIBSDIR)/Permutation_Type_solve.vo ll_cut.vo
lambek.vo: lambek.v $(OLLIBSDIR)/Injective.vo $(OLLIBSDIR)/List_more.vo $(OLLIBSDIR)/List_Type_more.vo ill_cut.vo



1 change: 0 additions & 1 deletion yalla/ll_smp.v
View file
Expand Up @@ -13,7 +13,6 @@ Require Import Permutation_Type_solve.

(** ** 0. load the [yalla] library *)

Require ll_cut.
Require ll_fragments.


Expand Down
3 changes: 1 addition & 2 deletions yalla/subs.v
View file
Expand Up @@ -5,9 +5,8 @@

(** * Substitutions in Linear Logic formulas and proofs *)

Require Import Permutation_Type.

Require Import List_more.
Require Import Permutation_Type.
Require Import genperm_Type.

Require Export ll_def.
Expand Down
11 changes: 7 additions & 4 deletions yalla/tl.v
View file
Expand Up @@ -256,15 +256,12 @@ Qed.
(** ** 4. characterize corresponding [ill] fragment *)

(*
Require Import ill_prop.
Lemma tl2ill_dec : forall A,
{B | A = tl2ill B} + (A = N)
+ ((forall B, A = tl2ill B -> False) * (A = N -> False)).
Proof with try reflexivity.
induction A ;
(try now (right ; intros B Heq ; destruct B ; inversion Heq))
;
(try now (right ; intros B Heq ; destruct B ; inversion Heq)) ;
try (destruct IHA1 as [[[B1 Heq1] | Hr1] | [Hr1 HN1]] ;
destruct IHA2 as [[[B2 Heq2] | Hr2] | [Hr2 HN2]] ; subst ;
(try now (right ; split ;
Expand All @@ -286,6 +283,7 @@ induction A ;
+ subst ; left ; left ; exists (tvar j)...
- left ; left ; exists tone...
- left ; left ; exists (ttens B1 B2)...
- right ; split ; [ intros B Heq ; destruct B | intros Heq ] ; inversion Heq.
- destruct IHA as [[[B Heq] | Hr] | [Hr HN]] ; subst.
+ left ; left ; exists (tneg B)...
+ right ; split ; [ intros B Heq ; destruct B | intros Heq ] ; inversion Heq.
Expand Down Expand Up @@ -330,6 +328,11 @@ induction Hsf ; unfold tl_fragment in HfA.
destruct s as [[B' Heq] | Heq] ; try destruct B' ; inversion Heq.
- destruct (tl2ill_dec (ilpam C B)) ; try now inversion HfA.
destruct s as [[B' Heq] | Heq] ; try destruct B' ; inversion Heq.
- destruct (tl2ill_dec (igen B)) ; try now inversion HfA.
destruct s as [[B' Heq] | Heq] ; try now inversion Heq.
destruct B' ; inversion Heq.
- unfold tl_fragment ; destruct (tl2ill_dec N)...
exfalso ; apply (snd p)...
- destruct (tl2ill_dec (ilmap B C)) ; try now inversion HfA.
destruct s as [[B' Heq] | Heq] ; try destruct B' ; inversion Heq.
- destruct (tl2ill_dec (ilmap C B)) ; try now inversion HfA.
Expand Down

0 comments on commit 51df5e9

Please sign in to comment.