Skip to content

Comparing changes

Choose two branches to see what’s changed or to start a new pull request. If you need to, you can also .

Open a pull request

Create a new pull request by comparing changes across two branches. If you need to, you can also .
...
  • 5 commits
  • 4 files changed
  • 0 commit comments
  • 2 contributors
Showing with 83 additions and 97 deletions.
  1. +3 −8 Make
  2. +3 −0 src/forcing_plugin.mllib
  3. +57 −72 test-suite/Basics.v
  4. +20 −17 theories/Init.v
View
11 Make
@@ -1,15 +1,10 @@
--I src -R theories Forcing
--custom "$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $^" "src/forcing_common.cmx src/forcing.cmx src/forcing_plugin_mod.cmx" src/forcing_plugin.cmxs
--custom "$(CAMLLINK) -g -a -o $@ $^" "src/forcing_common.cmo src/forcing.cmo src/forcing_plugin_mod.cmo" src/forcing_plugin.cma
--custom "$(COQBIN)coqc $(COQDEBUG) $(COQFLAGS) $(OTHERFLAGS) $*" "%.v $(UNICOQPLUGINOPT) $(UNICOQPLUGIN)" "%.vo %.glob"
+-I src
+-R theories Forcing
-custom "coqmktop -o $@ $^" "src/forcing_plugin.cma" coqtop
-UNICOQPLUGIN = "src/forcing_plugin.cma"
-UNICOQPLUGINOPT = "src/forcing_plugin.cmxs"
-COQDOC = "$(COQBIN)coqdoc -interpolate -utf8"
-CAMLP4OPTIONS = "-loc loc"
src/forcing_common.ml4
src/forcing.ml4
src/forcing_plugin_mod.ml
+src/forcing_plugin.mllib
theories/Init.v
theories/Forcing.v
#test-suite/Basics.v
View
3 src/forcing_plugin.mllib
@@ -0,0 +1,3 @@
+Forcing_common
+Forcing
+Forcing_plugin_mod
View
129 test-suite/Basics.v
@@ -4,22 +4,25 @@ Require Import RelationClasses.
Notation " '{Σ' x , y } " := (exist x y).
Notation " '(Σ' x , y ) " := (existT x y).
-Section Test.
+Import NatForcing.
+Import NatCondition.
+Open Scope forcing_scope.
- Import NatForcing.
- Import NatCondition.
- Open Scope forcing_scope.
Hint Extern 4 => progress (unfold le in *) : forcing.
Lemma subp_proof2 p (q : subp p) : ` q <= p. apply subp_proof. Defined.
Hint Resolve subp_proof2 : forcing.
Ltac forcing_le :=
match goal with
- |- ` ?x <= ?y =>
+ | |- le (@proj1_sig _ _ ?y) ?x =>
+ apply (proj2_sig y)
+ | |- ` ?x <= ?y =>
match type of x with
subp ?r => transitivity r
end
+ | |- le (@subp_proj ?x ?y) ?x =>
+ apply (proj2_sig y)
| |- subp_proj ?x <= ?y =>
match type of x with
subp ?r => transitivity r
@@ -28,18 +31,18 @@ Ltac forcing_le :=
Hint Extern 2 (_ <= _) => forcing_le : forcing.
- Obligation Tactic := program_simpl; auto with forcing.
+Obligation Tactic := program_simpl; forcing.
Program Definition later_sheaf_f {p : nat} (q : subp p) (T : sheaf q) : subp q -> Type :=
fun r =>
match r with
| 0 => unit
| S r' => sheaf_f T r'
end.
-Next Obligation of later_sheaf_f. unfold le. destruct r. simpl in *. subst x; auto with arith. Qed.
+Next Obligation of later_sheaf_f. unfold le. destruct r. simpl in *. subst x; forcing. Qed.
Program Definition subppred {q} (r : subp q) : subp q := pred r.
-Next Obligation. intros. destruct r. simpl in *. unfold le in *. destruct x; eauto with arith. Defined.
+Next Obligation. intros. destruct r. simpl in *. unfold le in *. destruct x; forcing. Defined.
Program Definition later_transp {p} (q : subp p) (T : sheaf q) : transport (later_sheaf_f q T) :=
λ (r : subp q) (t : subp r) (M : later_sheaf_f q T r),
@@ -49,7 +52,7 @@ Program Definition later_transp {p} (q : subp p) (T : sheaf q) : transport (late
| S t' => fun prf => Θ T (subppred r) t' _
end tprf.
-Next Obligation. intros. destruct r, t. destruct x; simpl in *; unfold le in *; eauto with arith. Defined.
+Next Obligation. intros. destruct r, t. destruct x; simpl in *; forcing. Defined.
Next Obligation.
destruct r as [[|r'] Hr]; simpl in *; unfold le in *.
@@ -104,13 +107,13 @@ Proof. red; intros.
simpl in *.
unfold compose in tr. unfold subppred.
simpl.
- assert(x <= ` q) by (unfold le in *; auto with arith; admit).
+ unfold Θ. simpl.
+ assert(x <= ` q) by forcing.
pose (x':={Σ x, H0}:subp q).
pose proof (tr x').
- unfold Θ. simpl.
- assert(r' <= x) by (unfold le in *; auto with arith; admit).
+ assert(r' <= x) by forcing.
pose (rs':={Σ r', H2}:subp x').
- specialize (H1 rs'). assert (s' <= r') by admit.
+ specialize (H1 rs'). assert (s' <= r') by forcing.
specialize (H1 ({Σ s', H3})).
unfold later_sheaf_f in x0.
simpl in x0. specialize (H1 x0).
@@ -125,17 +128,16 @@ Program Definition later_trans_impl : later_trans :=
Next Obligation of later_trans_impl.
red. intros. simpl.
- unfold sheafC. simpl.
+ unfold sheafC.
destruct arg as [sh [transp [rt tt]]].
simpl. unfold later_trans_sheaf. apply f_equal. apply sigma_eq.
unfold Θ. simpl.
extensionality s0.
extensionality t.
extensionality x.
destruct t.
- simpl.
destruct x0. reflexivity.
- apply f_equal.
+ simpl. apply f_equal.
destruct s0.
simpl. destruct x1; reflexivity.
Qed.
@@ -150,13 +152,13 @@ Implicit Arguments forcing_traduction [[A] [ForcingOp]].
Notation " '{Σ' x } " := (exist x _).
-Obligation Tactic := auto with forcing arith.
+Obligation Tactic := program_simpl; forcing.
Time Forcing Operator next : (forall T : Set, T -> later T).
Next Obligation.
- intros. red. simpl. intros r1.
- apply (proj2_sig f1 (one_trans _ _ _ r1)).
+ intros. red; simpl; intros.
+ apply (H (one_trans _ _ _ r1)).
Qed.
Notation ι r := (iota r).
@@ -212,78 +214,64 @@ Proof. Transparent later_transp.
rewrite H4.
reflexivity.
Qed.
-Unset Printing All.
-(* Needs eta *)
+Transparent later_transp.
+Program Definition nextdef p : { x | next_transprop1 p (iota_refl p) x } :=
+ @innernext p.
-Check (fun p (r : subp p) (q : subp r) =>
- eq_refl : (q : P) = (iota q : subp p)).
+Next Obligation of nextdef.
+Proof.
+ intros.
+ pose proof (proj2_sig (innernext x x0)).
+ red; intros.
+ specialize (H r1 s1 arg1).
+ simpl in H. simpl. now destruct s1.
+Qed.
-Next Obligation of next_inst.
+Next Obligation of nextdef.
Proof.
- red.
- simpl. intros.
- Program Definition foo p : { x | next_transprop1 p (iota_refl p) x } :=
- @innernext p.
- Next Obligation of foo.
- Proof. Transparent later_transp.
- intros.
- pose proof (proj2_sig (innernext x x0)).
- red; intros.
- specialize (H r1 s1 arg1).
- simpl in H. simpl. now destruct s1.
- Qed.
- Next Obligation of foo.
- Proof. Transparent later_transp.
- intros.
- red; intros.
+ intros.
+ red; intros.
apply sigma_eq.
apply functional_extensionality_dep.
simpl; intros.
destruct x as [[|x'] Hx]. simpl.
reflexivity.
simpl.
reflexivity.
- Qed.
-
- exact (foo p).
Qed.
-Forcing Operator fixp : (forall T : Type, (later T -> T) -> T).
+Next Obligation of next_inst.
+Proof nextdef.
-Next Obligation.
- intros.
- Example zero_trans p (q : subp p) (r : subp q) : subp p.
- Proof. exact (iota r). Defined.
+Forcing Operator fixp : (forall T : Type, (later T -> T) -> T).
- change ( fixp_transprop p q r arg q2 r1 (zero_trans _ _ r3) (λ s2 : subp (zero_trans _ _ r3), (` f2) (zero_trans _ r3 s2 : subp q4))).
- red.
- destruct f2 as [f2 Hf2].
+(** Should be automatable: simple reindexings of commutation
+ properties. *)
- simpl in *. red in Hf2; simpl in Hf2.
- intros; apply (Hf2 (iota r2) s2 arg2).
+Next Obligation.
+Proof.
+ red in H; simpl in H.
+ red; simpl; intros; apply (H (iota r2) s2 arg2).
Qed.
Next Obligation.
- intros.
- simpl.
red. simpl.
intros.
- simpl in *.
- unfold fixp_transprop1 in f1. simpl in f1.
- apply (proj2_sig f1 (iota r1) s1).
+ unfold fixp_transprop1 in H.
+ apply (H (iota r1) s1).
Qed.
Definition Pred (p : nat) := { x : nat | x < p }.
Program Definition Pred_to_sub (p : nat) (q : Pred p) : subp p := q.
Next Obligation of Pred_to_sub.
- destruct q. simpl. red; auto with arith.
+ destruct q; forcing.
Defined.
Program Definition succ_of_Pred (p : nat) (q : Pred p) : subp p := S q.
Next Obligation of succ_of_Pred.
- destruct q. simpl. auto with arith.
+ destruct q; forcing.
Defined.
Program Definition subp0 (p : nat) : subp p := 0.
@@ -374,9 +362,8 @@ Program Definition secondfn :=
Program Definition lift_subp {p} (q : subp p) : subp (S p) := q.
Program Definition lift_Pred {p} (q : Pred p) : Pred (S p) := q.
Next Obligation of lift_Pred.
- intros p [q Hq].
- simpl; unfold le in *; auto with arith.
- Qed.
+ destruct q as [q Hq]. forcing.
+Qed.
Lemma lift_subp_rect_aux {q : nat} (P : subp (S q) -> Type)
(p0 : P (subp0 (S q)))
@@ -387,6 +374,7 @@ Lemma lift_subp_rect_aux {q : nat} (P : subp (S q) -> Type)
Proof. induction r; simpl; auto.
apply f_equal. apply IHr.
Qed.
+
Program Definition subp_le {p} (q : subp p) r (prf : p <= r) : subp r := q.
Ltac forward H :=
@@ -396,22 +384,21 @@ Ltac forward H :=
end.
Next Obligation of secondfn.
- simpl; intros.
intros [r1 Hr1].
induction r1; simpl; intros.
unfold innerfn; simpl.
unfold Θ in *; simpl in *.
red in arg1.
(* 0 *)
- destruct s1 as [[|s1] Hs1].
- simpl.
- pose (proj2_sig arg1 (subp0 0) (subp0 _)). apply e.
+ destruct s1 as [[|s1] Hs1]; simpl.
+ apply (proj2_sig arg1 (subp0 0) (subp0 _)).
+
inversion Hs1.
(* S n *)
Transparent later_transp.
- forward IHr1; auto with arith forcing.
+ forward IHr1; forcing.
pose (proj2_sig arg1 (embed (S r1)) s1).
simpl in e.
unfold innerfn.
@@ -422,8 +409,8 @@ Next Obligation of secondfn.
simpl in *.
simpl.
- assert(s1 <= r1) by auto with forcing arith.
- assert(r1 <= r1) by reflexivity.
+ assert(s1 <= r1) by forcing.
+ assert(r1 <= r1) by forcing.
rewrite lift_subp_rect_aux with (prf':=H1).
rewrite lift_subp_rect_aux with (prf':=reflexivity s1 : s1 <= s1).
specialize (IHr1 {Σ s1, H0}).
@@ -440,5 +427,3 @@ Next Obligation.
exists (secondfn p).
red; intros. reflexivity.
Qed.
-
-End Test.
View
37 theories/Init.v
@@ -150,7 +150,9 @@ Module Forcing(F : Condition).
Local Open Scope forcing_scope.
- Definition subp (p : P) := { q : P | q <= p }.
+ Definition Psub (p : P) := fun q : P => q <= p.
+
+ Definition subp (p : P) := sig (Psub p).
Definition subp_proj {p : P} (q : subp p) : P := ` q.
Global Coercion subp_proj : subp >-> P.
@@ -163,10 +165,10 @@ Module Forcing(F : Condition).
Lemma subp_proof {p} (q : subp p) : (subp_proj q) <= p.
Proof. apply (proj2_sig q). Defined.
- Hint Resolve subp_proof.
+ Hint Resolve subp_proof : forcing.
Program Definition iota_refl p : subp p := p.
- Next Obligation. reflexivity. Qed.
+ Next Obligation. red; reflexivity. Qed.
(** We define an overloaded [ι] operator to infer canonical
coercions of conditions into larger subsets. *)
@@ -177,12 +179,19 @@ Module Forcing(F : Condition).
Global Implicit Arguments iota [[p] [q] [Iota]].
+
+ Hint Extern 0 (_ <= _) => apply reflexivity : forcing.
+ Hint Extern 0 (_ = _) => try f_equal ; reflexivity : forcing.
+
+ Ltac forcing :=
+ try solve [simpl; unfold Psub in *; auto with arith forcing].
+ Obligation Tactic := program_simpl; forcing.
+
(** The identity, in case no coercion was needed in fact *)
Global Program Instance iota_reflexive p (q : subp p) : Iota p q p := { iota := (q : P) }.
(** Self-indexing [q : P p] then [q : P q] *)
Global Program Instance iota_lift p (q : subp p) : Iota p q q := { iota := (q : P) }.
- Next Obligation. reflexivity. Defined.
(** [q : P p] so forall [r : P q] [r : P p] as well *)
Global Program Instance iota_pi {p} (q : subp p) : Iota q (iota q) p :=
@@ -192,7 +201,7 @@ Module Forcing(F : Condition).
Global Program Instance iota_pi_inv {p} (q : subp p) (r : subp q) : Iota q r p :=
{ iota := (r : P) }.
- Next Obligation. now transitivity q. Defined.
+ Next Obligation. red; transitivity q; auto with forcing. Defined.
(** Iotas compose *)
Program Definition iota_compose {p sp q r} (pq : Iota p sp q) (qr : Iota q (iota sp) r) : Iota p sp r :=
@@ -225,9 +234,6 @@ Module Forcing(F : Condition).
|- Iota ?p ?sp ?q => apply_iota_compose p sp q
end.
- Hint Extern 0 (_ <= _) => apply reflexivity : forcing.
- Hint Extern 0 (_ = _) => try f_equal ; reflexivity : forcing.
-
Goal forall p sp q r (iop : Iota p sp q), Iota q (iota sp) r -> Iota p sp r.
Proof. intros. typeclasses eauto. Qed.
@@ -256,13 +262,10 @@ Module Forcing(F : Condition).
Example four_trans p (q : subp p) (r : subp q) (s : subp r) (t : subp s) (u : subp t) (v : subp u)
: subp q.
- Proof. exact (iota v). Show Proof. Defined.
-
- Ltac prog_forcing := auto with forcing.
- Obligation Tactic := program_simpl ; prog_forcing.
-
- Section Translation.
+ Proof. exact (iota v). Defined.
+ Section Translation.
+
Definition transport {p} (f : subp p → Type) :=
forall q : subp p, forall r : subp q, arrow (f q) (f (iota r)).
@@ -271,11 +274,11 @@ Module Forcing(F : Condition).
Notation " 'rewrite' p 'in' x " := (eq_rect _ _ x _ p) (at level 10).
- Definition refl (Θ : transport f) :=
+ Definition refl (Θ : transport f) := Eval simpl in
forall q : subp p, forall x : f q,
Θ q (iota q) x = x.
- Definition trans (Θ : transport f) :=
+ Definition trans (Θ : transport f) := Eval simpl in
forall q : subp p, forall r : subp q, forall s : subp r,
forall x, ((Θ (iota r) s) ∘ (Θ q r)) x = Θ q (iota s) x.
@@ -320,7 +323,7 @@ Module Forcing(F : Condition).
intros. unfold compose. destruct f; simpl in *.
destruct s0 as [θ [Hr Ht]].
red in Ht. pose (Ht (iota q0) r0 s x). unfold compose in *. simpl in *.
- unfold Θ. simpl. rewrite <- e. destruct r0; reflexivity.
+ unfold Θ. simpl in *. rewrite <- e. destruct r0; reflexivity.
Qed.
End Translation.

No commit comments for this range

Something went wrong with that request. Please try again.