Skip to content
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

param1.inhab and failure to find param1 #408

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

param1.inhab and failure to find param1 #408

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
cb1d2bf
test
gares Nov 25, 2022
3dab459
some more digging
gares Nov 25, 2022
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
109 changes: 109 additions & 0 deletions apps/derive/tests/test_derive.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -168,3 +168,112 @@ Check Kwi _ (refl_equal 3).
From Coq Require Ascii.

#[only(param2)] derive Ascii.ascii.

(* #407 *)
Definition is_zero (n:nat) := match n with O => true | _ => false end.
derive is_zero.

Inductive toto1 := | Toto1 : forall n, unit -> is_zero n = true -> toto1.
Inductive toto2 := | Toto2 : forall n, is_zero n = true -> unit -> toto2.
Inductive toto3 := | Toto3 : unit -> forall n, is_zero n = true -> toto3.

#[only(param1_trivial)] derive toto1.
#[only(param1_trivial)] derive toto2.
Check
fun x : toto2 =>
contracts toto2 is_toto2 x (is_toto2_inhab x)
((fix IH (x0 : toto2) (y : is_toto2 x0) {struct y} : is_toto2_inhab x0 = y :=
match y as i in (is_toto2 s1) return (is_toto2_inhab s1 = i) with
| is_Toto2 n Pn x1 P_ x2 P_0 =>
match
trivial_uniq unit Prelude.is_unit Prelude.is_unit_trivial x2 P_0 as
i in (_ = H)
return
(_ =
is_Toto2 n Pn x1 P_ x2 H)
with
| eq_refl =>
match
trivial_uniq (is_zero n = true)
(is_eq bool is_bool (is_zero n) (is_is_zero n Pn) true
is_true)
(is_eq_trivial bool is_bool is_bool_trivial (is_zero n)
(is_is_zero n Pn) true is_true) x1 P_ as i in (_ = H)
return
(_ =
is_Toto2 n Pn x1 H x2
(trivial_full unit Prelude.is_unit Prelude.is_unit_trivial
x2))
with
| eq_refl =>
match
trivial_uniq nat is_nat is_nat_trivial n Pn as i in (_ = H)
return
(_ =
is_Toto2 n H x1
(trivial_full (is_zero n = true)
(is_eq bool is_bool (is_zero n) (is_is_zero n H)
true is_true)
(is_eq_trivial bool is_bool is_bool_trivial
(is_zero n) (is_is_zero n H) true is_true) x1)
x2
(trivial_full unit Prelude.is_unit
Prelude.is_unit_trivial x2))
with
| eq_refl => eq_refl
end
end
end
end) x).

#[only(param1)] derive toto3.
#[only(param1_inhab)] derive toto3.

Check
fun x : toto3 =>
contracts toto3 is_toto3 x (is_toto3_inhab x)
((fix IH (x0 : toto3) (y : is_toto3 x0) {struct y} : is_toto3_inhab x0 = y :=
match y as i in (is_toto3 s1) return (is_toto3_inhab s1 = i) with
| is_Toto3 x1 P_ n Pn x2 P_0 =>
match
trivial_uniq (is_zero n = true)
(is_eq bool is_bool (is_zero n) (is_is_zero n Pn) true is_true)
(is_eq_trivial bool is_bool is_bool_trivial (is_zero n)
(is_is_zero n Pn) true is_true) x2 P_0 as i in (_ = H)
return
(_ =
is_Toto3 x1 P_ n Pn x2 H)
with
| eq_refl =>
match
trivial_uniq nat is_nat is_nat_trivial n Pn as i in (_ = H)
return
(_ =
is_Toto3 x1 P_ n H x2
(trivial_full (is_zero n = true)
(is_eq bool is_bool (is_zero n) (is_is_zero n H) true
is_true)
(is_eq_trivial bool is_bool is_bool_trivial (is_zero n)
(is_is_zero n H) true is_true) x2))
with
| eq_refl =>
match
trivial_uniq unit Prelude.is_unit Prelude.is_unit_trivial
x1 P_ as i in (_ = H)
return
(_ =
is_Toto3 x1 H n
(trivial_full nat is_nat is_nat_trivial n) x2
(trivial_full (is_zero n = true)
(is_eq bool is_bool (is_zero n) (is_is_zero n Pn)
true is_true)
(is_eq_trivial bool is_bool is_bool_trivial
(is_zero n) (is_is_zero n Pn) true is_true) x2))
with
| eq_refl => eq_refl
end
end
end
end) x).

#[only(param1_trivial)] derive toto3.