Skip to content

Commit

Permalink
Merge pull request #38 from math-comp/remove-zify-ratify
Browse files Browse the repository at this point in the history
Remove zify_ring, zify_field, and ratify_field for the moment
  • Loading branch information
pi8027 authored Dec 14, 2021
2 parents ea94642 + a80e9f3 commit 2a4ef98
Show file tree
Hide file tree
Showing 6 changed files with 6 additions and 421 deletions.
3 changes: 0 additions & 3 deletions Make
Original file line number Diff line number Diff line change
@@ -1,7 +1,4 @@
theories/ratify_field.v
theories/ring.v
theories/zify_field.v
theories/zify_ring.v

-R theories mathcomp.algebra_tactics
-arg -w -arg -notation-overridden
Expand Down
1 change: 1 addition & 0 deletions Makefile.coq.local
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
theories/ring.vo : $(wildcard theories/*.elpi)
10 changes: 5 additions & 5 deletions examples/field_examples.v
Original file line number Diff line number Diff line change
@@ -1,12 +1,12 @@
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat choice seq.
From mathcomp Require Import fintype finfun bigop order ssralg ssrnum ssrint rat.
From mathcomp Require Import ring zify_ring.
From mathcomp Require Import ring.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Import GRing.Theory.
Import GRing.Theory Num.Theory.

Local Open Scope ring_scope.

Expand Down Expand Up @@ -34,8 +34,8 @@ Proof. by move=> F n n_neq0; field. Qed.

Goal forall (F : numFieldType) (n : nat),
n != 1%N -> ((n ^ 2)%:R - 1) / (n%:R - 1) = (n%:R + 1) :> F.
Proof. by move=> F n n_neq0; field; ring_lia. Qed.
Proof. by move=> F n n_neq0; field; rewrite subr_eq0 pnatr_eq1. Qed.

Goal forall (F : numFieldType) (n : nat),
n != 1%N -> (2%:R - (2 * n)%:R) / (1 - n%:R) = 2%:R :> F.
Proof. by move=> F n n_neq0; field; ring_lia. Qed.
n != 1%N -> (2%:R - (2 * n)%:R) / (1 - n%:R) = 2%:R :> F.
Proof. by move=> F n n_neq0; field; rewrite subr_eq0 eq_sym pnatr_eq1. Qed.
102 changes: 0 additions & 102 deletions theories/ratify_field.v

This file was deleted.

214 changes: 0 additions & 214 deletions theories/zify_field.v

This file was deleted.

Loading

0 comments on commit 2a4ef98

Please sign in to comment.