Skip to content

Pr156 #159

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
Casteran wants to merge 12 commits into
base: master
Choose a base branch
from
Draft

Pr156 #159

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
12 commits
Select commit Hold shift + click to select a range
eb463f5
Simplify a proof in Schutte/AP.v
Columbus240 Aug 18, 2023
89f48b9
Remove `In_full` from Schutte_basics
Columbus240 Aug 19, 2023
5069051
Move an `Arguments` statement to declaring file
Columbus240 Aug 19, 2023
350d847
Remove trailing whitespace in ordinals/Schutte
Columbus240 Aug 19, 2023
d8c46e6
Add coq-zorns-lemma as dependency
Columbus240 Aug 19, 2023
33cc798
Import `EnsemblesImplicit` in Schutte/PartialFun
Columbus240 Aug 19, 2023
6e50bea
Use ZornsLemma for def of Countable sets
Columbus240 Jul 30, 2023
893ba7e
Adopt coq-zorns-lemma.10.2.0
Columbus240 Aug 19, 2023
dc93bd2
Remove `countable` notation. Use `Countable`
Columbus240 Aug 20, 2023
1bdc7e3
Remove `countable_singleton`,use from `ZornsLemma`
Columbus240 Aug 20, 2023
b38f24b
try to update meta.yml
Casteran Sep 5, 2023
175a5b5
Add locality to Hint commands
Casteran Sep 11, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions coq-hydra-battles.opam
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,7 @@ depends: [
"dune" {>= "2.5"}
"coq" {(>= "8.14" & < "8.18~") | (= "dev")}
"coq-equations" {(>= "1.2" & < "1.4~") | (= "dev")}
"coq-zorns-lemma" { >= "10.2.0" }
"coq-libhyps"
]

Expand Down
5 changes: 5 additions & 0 deletions meta.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -166,6 +166,11 @@ dependencies:
version: '{= "dev"}'
description: |-
[CoqPrime](https://github.com/thery/coqprime)
- opam:
name: coq-zorns-lemma
version: '{>= "10.2.0"}'
description: |-
[zorns lemma](https://github.com/coq-community/topology)

namespace: hydras

Expand Down
4 changes: 2 additions & 2 deletions theories/ordinals/Epsilon0/Canon.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1039,7 +1039,7 @@ Proof.
destruct k; apply E0_eq_intro; reflexivity.
Qed.

Hint Rewrite Canon_Omega : E0_rw.
#[export] Hint Rewrite Canon_Omega : E0_rw.

Lemma CanonSSn (i:nat) :
forall alpha n , alpha <> E0zero ->
Expand Down Expand Up @@ -1095,7 +1095,7 @@ Proof.
simpl; apply T1limit_canonS_not_zero; auto.
Qed.

#[global]
#[export]
Hint Resolve CanonS_lt Canon_lt Canon_of_limit_not_null : E0.

Lemma CanonS_phi0_Succ alpha i : CanonS (E0phi0 (E0succ alpha)) i =
Expand Down
2 changes: 1 addition & 1 deletion theories/ordinals/Epsilon0/Hprime.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -94,7 +94,7 @@ Proof.
- apply Succ_Succb.
Qed.

Hint Rewrite H'_eq1 H'_eq2 : H'_rw.
#[export] Hint Rewrite H'_eq1 H'_eq2 : H'_rw.

Ltac lim_rw alpha := (assert (E0limit alpha) by auto with E0);
rewrite (H'_eq3 alpha); auto with E0.
Expand Down
4 changes: 2 additions & 2 deletions theories/ordinals/Epsilon0/L_alpha.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ From Equations Require Import Equations.
Import RelationClasses Relations.

#[global] Instance Olt : WellFounded E0lt := E0lt_wf.
#[global] Hint Resolve Olt : E0.
#[export] Hint Resolve Olt : E0.

(** Using Coq-Equations for building a function which satisfies
[Large_sets.L_spec] *)
Expand Down Expand Up @@ -68,7 +68,7 @@ Proof.
Qed.


Hint Rewrite L_zero_eqn L_succ_eqn : L_rw.
#[export] Hint Rewrite L_zero_eqn L_succ_eqn : L_rw.

(* begin snippet Paraphrasesc:: no-out *)
Lemma L_lim_eqn alpha i :
Expand Down
2 changes: 1 addition & 1 deletion theories/ordinals/Gamma0/Gamma0.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1096,7 +1096,7 @@ Module Gamma0_prec <: Precedence.
intros s; destruct s; simpl; trivial.
Qed.

Lemma prec_transitive : transitive A prec.
Lemma prec_transitive : transitive prec.
Proof.
intros s1 s2 s3; destruct s1; destruct s2; destruct s3;
simpl; intros; trivial; contradiction.
Expand Down
Loading